| author | paulson | 
| Wed, 23 Mar 2005 12:08:27 +0100 | |
| changeset 15618 | 05bad476e0f0 | 
| parent 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 | 
| 2650 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 5 | # | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 6 | # configure - adapt Isabelle distribution to system environment | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 7 | |
| 2655 | 8 | ## patch scripts | 
| 9 | ||
| 10511 | 10 | cd "`dirname "$0"`" | 
| 9915 | 11 | |
| 6029 | 12 | if bash -c : | 
| 2650 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 13 | then | 
| 10077 | 14 | bash lib/scripts/patch-scripts.bash | 
| 2650 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 15 | else | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 16 | echo "FATAL ERROR: bash not found!" | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 17 | exit 2 | 
| 
96234bf96bf9
configure - adapt Isabelle distribution to system environment
 wenzelm parents: diff
changeset | 18 | fi |