configure
author wenzelm
Fri, 05 Jun 1998 14:22:11 +0200
changeset 4992 c63a93b8577c
parent 3007 e5efa177ee0c
child 6029 30c957a74803
permissions -rwxr-xr-x
added THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq; added ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq; added APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq; added EVERY: ('a -> 'a seq) list -> 'a -> 'a seq; added FIRST: ('a -> 'b seq) list -> 'a -> 'b seq; added TRY: ('a -> 'a seq) -> 'a -> 'a seq; added REPEAT: ('a -> 'a seq) -> 'a -> 'a seq;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2650
96234bf96bf9 configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff changeset
     1
#!/bin/sh
96234bf96bf9 configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff changeset
     2
#
96234bf96bf9 configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff changeset
     3
# $Id$
96234bf96bf9 configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff changeset
     4
#
96234bf96bf9 configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff changeset
     5
# configure - adapt Isabelle distribution to system environment
96234bf96bf9 configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff changeset
     6
2655
9420efbb868e manual steps comment;
wenzelm
parents: 2650
diff changeset
     7
## patch scripts
9420efbb868e manual steps comment;
wenzelm
parents: 2650
diff changeset
     8
3007
e5efa177ee0c removed -norc;
wenzelm
parents: 2754
diff changeset
     9
if bash -c ""
2650
96234bf96bf9 configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff changeset
    10
then
96234bf96bf9 configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff changeset
    11
  bash lib/scripts/patch-scripts.bash
96234bf96bf9 configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff changeset
    12
else
96234bf96bf9 configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff changeset
    13
  echo "FATAL ERROR: bash not found!"
96234bf96bf9 configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff changeset
    14
  exit 2
96234bf96bf9 configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff changeset
    15
fi