install-personal-linux32.sh 1.3 KB

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152
  1. #! /bin/bash
  2. #
  3. # Install REDUCE in a dircetory that the user specifies
  4. #
  5. echo "This will install REDUCE. Please specify a directory"
  6. echo "that you would like the REDUCE files put in. This"
  7. echo "directory will end up containing several files and"
  8. echo "subdirectories..."
  9. echo ""
  10. # I use "bash" not just plain "sh" since I want to use "read" with
  11. # a "-p" (prompt) parameter... Also this is mostly for Linux so I
  12. # feel happy assuming "bash" is installed.
  13. read -p "Directory: " dest
  14. # What the user types is not processed at all by "read", but a user may feel
  15. # entitled to enter things like "~/dir" or "$MYDIR/path" and certainly for
  16. # the letter to work I need the next line here.
  17. dest=`eval echo $dest`
  18. if test -a $dest; then
  19. if test -d $dest; then
  20. echo "Will install in $dest"
  21. else
  22. echo "$dest exists but is not a directory."
  23. echo "Unable to proceed."
  24. exit 1
  25. fi
  26. else
  27. echo "Directory $dest does not exist."
  28. read -p "Shall I create it? (yes/no): " response
  29. if test "x$response" != "xyes"; then
  30. echo "Abandoning installation attempt."
  31. exit 1
  32. fi
  33. # Here I need to try to create the directory
  34. echo "Creating $dest for you..."
  35. mkdir -p $dest
  36. fi
  37. cp -pr ./r38.img ./r38.doc ./tests ./util ./testall.sh ./checkall.sh $dest
  38. ./relink.sh $dest
  39. echo "Reduce should now be available in $dest"
  40. echo "You may wish to add that directory to your PATH"
  41. exit 0