| author | streckem |
| Fri, 08 Aug 2003 14:57:46 +0200 | |
| changeset 14142 | 0b04f6587e67 |
| parent 10511 | efb3428c9879 |
| child 14981 | e73f8140af78 |
| 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