added POLYML_LINK_OPTIONS, which is required for unusual platforms (notably cygwin);
authorwenzelm
Wed, 29 Aug 2007 22:47:01 +0200
changeset 24479 b272d7998193
parent 24478 fb5e3fcfc10c
child 24480 97c0ef49fa8f
added POLYML_LINK_OPTIONS, which is required for unusual platforms (notably cygwin);
etc/settings
lib/scripts/run-polyml-5.0
lib/scripts/run-polyml-5.1
--- a/etc/settings	Wed Aug 29 20:18:23 2007 +0200
+++ b/etc/settings	Wed Aug 29 22:47:01 2007 +0200
@@ -30,11 +30,18 @@
 ML_OPTIONS="-H 500"
 ML_DBASE=""
 
-# Poly/ML 5.0
+# Poly/ML 5.1 on 64bit Linux
 #ML_PLATFORM=x86_64-linux
 #ML_HOME=/usr/local/polyml/x86_64-linux
-#ML_SYSTEM=polyml-5.0
+#ML_SYSTEM=polyml-5.1
+#ML_OPTIONS="-H 1000"
+
+# Poly/ML 5.1 on Cygwin
+#ML_PLATFORM=x86-cygwin
+#ML_HOME=/usr/local/polyml/x86-cygwin
+#ML_SYSTEM=polyml-5.1
 #ML_OPTIONS="-H 500"
+#POLYML_LINK_OPTIONS="-lstdc++"
 
 # Poly/ML 4.2.0
 #ML_PLATFORM=x86-linux
--- a/lib/scripts/run-polyml-5.0	Wed Aug 29 20:18:23 2007 +0200
+++ b/lib/scripts/run-polyml-5.0	Wed Aug 29 22:47:01 2007 +0200
@@ -87,7 +87,7 @@
 
 if [ -n "$OUTFILE" ]; then
   if [ -e "${OUTFILE}.o" ]; then
-    cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml || fail_out
+    cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml $POLYML_LINK_OPTIONS || fail_out
     rm -f "${OUTFILE}.o"
     [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
   fi
--- a/lib/scripts/run-polyml-5.1	Wed Aug 29 20:18:23 2007 +0200
+++ b/lib/scripts/run-polyml-5.1	Wed Aug 29 22:47:01 2007 +0200
@@ -87,7 +87,7 @@
 
 if [ -n "$OUTFILE" ]; then
   if [ -e "${OUTFILE}.o" ]; then
-    cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml || fail_out
+    cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml $POLYML_LINK_OPTIONS || fail_out
     rm -f "${OUTFILE}.o"
     [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
   fi