moved configure to lib/scripts;
authorwenzelm
Mon Jun 20 16:41:47 2005 +0200 (2005-06-20)
changeset 16477e1a36498a30f
parent 16476 baa008d0fee9
child 16478 d0a1f6231e2f
moved configure to lib/scripts;
configure
lib/scripts/configure
     1.1 --- a/configure	Mon Jun 20 16:41:20 2005 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,18 +0,0 @@
     1.4 -#!/bin/sh
     1.5 -#
     1.6 -# $Id$
     1.7 -# Author: Markus Wenzel, TU Muenchen
     1.8 -#
     1.9 -# configure - adapt Isabelle distribution to system environment
    1.10 -
    1.11 -## patch scripts
    1.12 -
    1.13 -cd "`dirname "$0"`"
    1.14 -
    1.15 -if bash -c :
    1.16 -then
    1.17 -  bash lib/scripts/patch-scripts.bash
    1.18 -else
    1.19 -  echo "FATAL ERROR: bash not found!"
    1.20 -  exit 2
    1.21 -fi
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/lib/scripts/configure	Mon Jun 20 16:41:47 2005 +0200
     2.3 @@ -0,0 +1,18 @@
     2.4 +#!/bin/sh
     2.5 +#
     2.6 +# $Id$
     2.7 +# Author: Markus Wenzel, TU Muenchen
     2.8 +#
     2.9 +# configure - adapt Isabelle distribution to system environment
    2.10 +
    2.11 +## patch scripts
    2.12 +
    2.13 +cd "`dirname "$0"`"
    2.14 +
    2.15 +if bash -c :
    2.16 +then
    2.17 +  bash lib/scripts/patch-scripts.bash
    2.18 +else
    2.19 +  echo "FATAL ERROR: bash not found!"
    2.20 +  exit 2
    2.21 +fi