diff options
Diffstat (limited to 'source4/script/installheader.sh')
| -rwxr-xr-x | source4/script/installheader.sh | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/source4/script/installheader.sh b/source4/script/installheader.sh deleted file mode 100755 index 9aed5ed1c3..0000000000 --- a/source4/script/installheader.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/bin/sh - -INCLUDEDIR=$1 -shift - -for p in $*; do - p2=`basename $p` - echo Installing $p as $INCLUDEDIR/$p2 - if [ -f $INCLUDEDIR/$p2 ]; then - rm -f $INCLUDEDIR/$p2.old - mv $INCLUDEDIR/$p2 $INCLUDEDIR/$p2.old - fi - cp $p $INCLUDEDIR/ - -done - -cat << EOF -====================================================================== -The headers are installed. You may restore the old headers (if there -were any) using the command "make revert". You may uninstall the headers -using the command "make uninstallheader" or "make uninstall" to uninstall -binaries, man pages and shell scripts. -====================================================================== -EOF - -exit 0 |