equal
deleted
inserted
replaced
|
1 # -*- shell-script -*- :mode=shellscript: |
|
2 |
|
3 # basic settings |
|
4 |
|
5 #ML_SYSTEM=polyml-5.4.1 |
|
6 #ML_PLATFORM="$ISABELLE_PLATFORM" |
|
7 #ML_HOME="$COMPONENT/$ML_PLATFORM" |
|
8 #ML_OPTIONS="-H 500" |
|
9 #ML_SOURCES="$ML_HOME/../src" |
|
10 |
|
11 |
|
12 # smart settings |
|
13 |
|
14 ML_SYSTEM=polyml-5.4.1 |
|
15 |
|
16 case "$ISABELLE_PLATFORM" in |
|
17 *-linux) |
|
18 if env LD_LIBRARY_PATH="$COMPONENT/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \ |
|
19 "$COMPONENT/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null |
|
20 then |
|
21 ML_PLATFORM="$ISABELLE_PLATFORM32" |
|
22 else |
|
23 echo >&2 "### Cannot execute Poly/ML in 32bit mode -- using bulky 64bit version instead" |
|
24 ML_PLATFORM="$ISABELLE_PLATFORM64" |
|
25 fi |
|
26 ;; |
|
27 *) |
|
28 ML_PLATFORM="$ISABELLE_PLATFORM32" |
|
29 ;; |
|
30 esac |
|
31 |
|
32 case "$ML_PLATFORM" in |
|
33 x86_64-*) |
|
34 ML_OPTIONS="-H 1000" |
|
35 ;; |
|
36 *) |
|
37 ML_OPTIONS="-H 500" |
|
38 ;; |
|
39 esac |
|
40 |
|
41 ML_HOME="$COMPONENT/$ML_PLATFORM" |
|
42 ML_SOURCES="$COMPONENT/src" |
|
43 |