equal
deleted
inserted
replaced
101 *) |
101 *) |
102 POLYML_EXE="$ML_HOME/poly" |
102 POLYML_EXE="$ML_HOME/poly" |
103 ;; |
103 ;; |
104 esac |
104 esac |
105 |
105 |
106 #ML system identifier |
|
107 if [ -z "$ML_PLATFORM" ]; then |
|
108 ML_IDENTIFIER="$ML_SYSTEM" |
|
109 else |
|
110 ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}" |
|
111 fi |
|
112 |
|
113 #enforce ISABELLE_OCAMLFIND |
106 #enforce ISABELLE_OCAMLFIND |
114 if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]; then |
107 if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]; then |
115 ISABELLE_OCAMLFIND="$ISABELLE_HOME/lib/scripts/ocamlfind" |
108 ISABELLE_OCAMLFIND="$ISABELLE_HOME/lib/scripts/ocamlfind" |
116 fi |
109 fi |
117 |
110 |