equal
deleted
inserted
replaced
1 #!/bin/sh |
1 #!/bin/sh |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # |
4 # |
5 # configure - adapt Isabelle distribution to system environment |
5 # configure - adapt Isabelle distribution to system environment |
|
6 |
|
7 ## patch scripts |
6 |
8 |
7 if bash -norc -c "" |
9 if bash -norc -c "" |
8 then |
10 then |
9 bash lib/scripts/patch-scripts.bash |
11 bash lib/scripts/patch-scripts.bash |
10 else |
12 else |
11 echo "FATAL ERROR: bash not found!" |
13 echo "FATAL ERROR: bash not found!" |
12 exit 2 |
14 exit 2 |
13 fi |
15 fi |
|
16 |
|
17 |
|
18 ## manual steps |
|
19 |
|
20 PWD=`pwd` |
|
21 echo |
|
22 echo "***********************************************************" |
|
23 echo "* Please check the ML compiler settings in ./etc/settings *" |
|
24 echo "* before compiling Isabelle. *" |
|
25 echo "***********************************************************" |
|
26 echo |