author | wenzelm |
Thu, 21 Sep 2000 15:58:13 +0200 | |
changeset 10052 | 5fa8d8d5c852 |
parent 9915 | 8de4ea6de3d0 |
child 10077 | 0261aede52ca |
permissions | -rwxr-xr-x |
#!/bin/sh # # $Id$ # Author: Markus Wenzel, TU Muenchen # License: GPL (GNU GENERAL PUBLIC LICENSE) # # configure - adapt Isabelle distribution to system environment ## patch scripts THIS=`dirname "$0"` if bash -c : then bash "$THIS/lib/scripts/patch-scripts.bash" else echo "FATAL ERROR: bash not found!" exit 2 fi