#!/bin/sh # # $Id: configure,v 1.1 2005/06/20 14:41:47 wenzelm Exp $ # Author: Markus Wenzel, TU Muenchen # # 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