2 # this script courtesy of James_K._Foote.PARC@xerox.com
3 # 5 July 96 Dan.Shearer@UniSA.Edu.Au Don't hardcode script names, get from Make
11 echo Installing scripts in $BINDIR
17 echo Failed to make directory $d
18 echo Have you run installbin first?
26 echo Installing $BINDIR/$p2
27 if [ -f $BINDIR/$p2 ]; then
28 mv $BINDIR/$p2 $BINDIR/$p2.old
31 chmod $INSTALLPERMS $BINDIR/$p2
32 if [ ! -f $BINDIR/$p2 ]; then
33 echo Cannot copy $p2... does $USER have privileges?
38 ======================================================================
39 The scripts have been installed. You may uninstall them using
40 the command "make uninstallscripts" or "make install" to install binaries,
41 man pages and shell scripts. You may recover the previous version (if any
43 ======================================================================