| author | streckem | 
| Mon, 26 May 2003 18:36:15 +0200 | |
| changeset 14045 | a34d89ce6097 | 
| parent 10511 | efb3428c9879 | 
| child 14981 | e73f8140af78 | 
| permissions | -rwxr-xr-x | 
| 2650 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 1 | #!/bin/sh | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 2 | # | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 3 | # $Id$ | 
| 9818 | 4 | # Author: Markus Wenzel, TU Muenchen | 
| 5 | # License: GPL (GNU GENERAL PUBLIC LICENSE) | |
| 2650 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 6 | # | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 7 | # configure - adapt Isabelle distribution to system environment | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 8 | |
| 2655 | 9 | ## patch scripts | 
| 10 | ||
| 10511 | 11 | cd "`dirname "$0"`" | 
| 9915 | 12 | |
| 6029 | 13 | if bash -c : | 
| 2650 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 14 | then | 
| 10077 | 15 | bash lib/scripts/patch-scripts.bash | 
| 2650 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 16 | else | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 17 | echo "FATAL ERROR: bash not found!" | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 18 | exit 2 | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 19 | fi |