equal
deleted
inserted
replaced
|
1 #!/bin/sh |
|
2 # |
|
3 # $Id$ |
|
4 # |
|
5 # configure - adapt Isabelle distribution to system environment |
|
6 |
|
7 if bash -norc -c "" |
|
8 then |
|
9 bash lib/scripts/patch-scripts.bash |
|
10 else |
|
11 echo "FATAL ERROR: bash not found!" |
|
12 exit 2 |
|
13 fi |