wenzelm@2650: #!/bin/sh
wenzelm@2650: #
wenzelm@2650: # $Id$
wenzelm@9818: # Author: Markus Wenzel, TU Muenchen
wenzelm@9818: # License: GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@2650: #
wenzelm@2650: # configure - adapt Isabelle distribution to system environment
wenzelm@2650: 
wenzelm@2655: ## patch scripts
wenzelm@2655: 
wenzelm@10511: cd "`dirname "$0"`"
wenzelm@9915: 
wenzelm@6029: if bash -c :
wenzelm@2650: then
wenzelm@10077:   bash lib/scripts/patch-scripts.bash
wenzelm@2650: else
wenzelm@2650:   echo "FATAL ERROR: bash not found!"
wenzelm@2650:   exit 2
wenzelm@2650: fi