blob: 9aed5ed1c3c9dd58bedddce227cc84b040644b0a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
#!/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
|
