equal
deleted
inserted
replaced
11 bash lib/scripts/patch-scripts.bash |
11 bash lib/scripts/patch-scripts.bash |
12 else |
12 else |
13 echo "FATAL ERROR: bash not found!" |
13 echo "FATAL ERROR: bash not found!" |
14 exit 2 |
14 exit 2 |
15 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 |
|