equal
deleted
inserted
replaced
1 # -*- shell-script -*- :mode=shellscript: |
1 # -*- shell-script -*- :mode=shellscript: |
|
2 |
|
3 POLYML_HOME="$COMPONENT" |
|
4 |
2 |
5 |
3 # basic settings |
6 # basic settings |
4 |
7 |
5 #ML_SYSTEM=polyml-5.5.0 |
8 #ML_SYSTEM=polyml-5.5.1 |
6 #ML_PLATFORM="$ISABELLE_PLATFORM" |
9 #ML_PLATFORM="$ISABELLE_PLATFORM32" |
7 #ML_HOME="$COMPONENT/$ML_PLATFORM" |
10 #ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
8 #ML_OPTIONS="-H 500" |
11 #ML_OPTIONS="-H 500" |
9 #ML_SOURCES="$ML_HOME/../src" |
12 #ML_SOURCES="$POLYML_HOME/src" |
10 |
13 |
11 |
14 |
12 # smart settings |
15 # smart settings |
13 |
16 |
14 ML_SYSTEM=polyml-5.5.0 |
17 ML_SYSTEM=polyml-5.5.1 |
15 |
18 |
16 case "$ISABELLE_PLATFORM" in |
19 case "$ISABELLE_PLATFORM" in |
17 *-linux) |
20 *-linux) |
18 if env LD_LIBRARY_PATH="$COMPONENT/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \ |
21 if env LD_LIBRARY_PATH="$POLYML_HOME/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \ |
19 "$COMPONENT/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null |
22 "$POLYML_HOME/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null |
20 then |
23 then |
21 ML_PLATFORM="$ISABELLE_PLATFORM32" |
24 ML_PLATFORM="$ISABELLE_PLATFORM32" |
22 else |
25 else |
23 ML_PLATFORM="$ISABELLE_PLATFORM64" |
26 ML_PLATFORM="$ISABELLE_PLATFORM64" |
24 if [ -z "$ML_PLATFORM_FALLBACK" ]; then |
27 if [ -z "$ML_PLATFORM_FALLBACK" ]; then |
40 *) |
43 *) |
41 ML_OPTIONS="-H 500" |
44 ML_OPTIONS="-H 500" |
42 ;; |
45 ;; |
43 esac |
46 esac |
44 |
47 |
45 ML_HOME="$COMPONENT/$ML_PLATFORM" |
48 ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
46 ML_SOURCES="$COMPONENT/src" |
49 ML_SOURCES="$POLYML_HOME/src" |
47 |
50 |