| author | wenzelm | 
| Thu, 28 Sep 2000 19:07:09 +0200 | |
| changeset 10111 | 78a0397eaec1 | 
| parent 10077 | 0261aede52ca | 
| child 10511 | efb3428c9879 | 
| 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 cd `dirname "$0"` if bash -c : then bash lib/scripts/patch-scripts.bash else echo "FATAL ERROR: bash not found!" exit 2 fi