equal
deleted
inserted
replaced
18 if env LD_LIBRARY_PATH="$COMPONENT/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \ |
18 if env LD_LIBRARY_PATH="$COMPONENT/$ISABELLE_PLATFORM32:$LD_LIBRARY_PATH" \ |
19 "$COMPONENT/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null |
19 "$COMPONENT/$ISABELLE_PLATFORM32/poly" -v >/dev/null 2>/dev/null |
20 then |
20 then |
21 ML_PLATFORM="$ISABELLE_PLATFORM32" |
21 ML_PLATFORM="$ISABELLE_PLATFORM32" |
22 else |
22 else |
23 echo >&2 "### Cannot execute Poly/ML in 32bit mode: missing shared libraries for C/C++" |
|
24 echo >&2 "### Using more voluminous 64bit version of Poly/ML instead" |
|
25 ML_PLATFORM="$ISABELLE_PLATFORM64" |
23 ML_PLATFORM="$ISABELLE_PLATFORM64" |
|
24 if [ -z "$ML_PLATFORM_FALLBACK" ]; then |
|
25 echo >&2 "### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++)" |
|
26 echo >&2 "### Using bulky 64bit version of Poly/ML instead" |
|
27 ML_PLATFORM_FALLBACK="true" |
|
28 fi |
26 fi |
29 fi |
27 ;; |
30 ;; |
28 *) |
31 *) |
29 ML_PLATFORM="$ISABELLE_PLATFORM32" |
32 ML_PLATFORM="$ISABELLE_PLATFORM32" |
30 ;; |
33 ;; |