lib/scripts/configure
changeset 16477 e1a36498a30f
equal deleted inserted replaced
16476:baa008d0fee9 16477:e1a36498a30f
       
     1 #!/bin/sh
       
     2 #
       
     3 # $Id$
       
     4 # Author: Markus Wenzel, TU Muenchen
       
     5 #
       
     6 # configure - adapt Isabelle distribution to system environment
       
     7 
       
     8 ## patch scripts
       
     9 
       
    10 cd "`dirname "$0"`"
       
    11 
       
    12 if bash -c :
       
    13 then
       
    14   bash lib/scripts/patch-scripts.bash
       
    15 else
       
    16   echo "FATAL ERROR: bash not found!"
       
    17   exit 2
       
    18 fi