author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 10511 | efb3428c9879 |
permissions | -rwxr-xr-x |
1 #!/bin/sh
2 #
3 # $Id$
4 # Author: Markus Wenzel, TU Muenchen
5 #
6 # configure - adapt Isabelle distribution to system environment
8 ## patch scripts
10 cd "`dirname "$0"`"
12 if bash -c :
13 then
14 bash lib/scripts/patch-scripts.bash
15 else
16 echo "FATAL ERROR: bash not found!"
17 exit 2
18 fi