| author | wenzelm |
| Mon, 17 Feb 1997 17:22:19 +0100 | |
| changeset 2650 | 96234bf96bf9 |
| child 2655 | 9420efbb868e |
| permissions | -rwxr-xr-x |
|
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 |
|
|
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
7 |
if bash -norc -c "" |
|
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
8 |
then |
|
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
9 |
bash lib/scripts/patch-scripts.bash |
|
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
10 |
else |
|
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
11 |
echo "FATAL ERROR: bash not found!" |
|
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
12 |
exit 2 |
|
96234bf96bf9
configure - adapt Isabelle distribution to system environment
wenzelm
parents:
diff
changeset
|
13 |
fi |