equal
deleted
inserted
replaced
30 ML_OPTIONS="-H 80" |
30 ML_OPTIONS="-H 80" |
31 ML_DBASE="" |
31 ML_DBASE="" |
32 |
32 |
33 # Poly/ML 4.2.0 (manual settings) |
33 # Poly/ML 4.2.0 (manual settings) |
34 #ML_PLATFORM=x86-linux |
34 #ML_PLATFORM=x86-linux |
35 #ML_HOME=/usr/local/polyml/x86-linux" |
35 #ML_HOME=/usr/local/polyml/x86-linux |
36 #ML_SYSTEM=polyml-4.2.0 |
36 #ML_SYSTEM=polyml-4.2.0 |
37 #ML_OPTIONS="-H 80" |
37 #ML_OPTIONS="-H 80" |
38 |
38 |
39 # Standard ML of New Jersey 110 or later |
39 # Standard ML of New Jersey 110 or later |
40 #SMLNJ_CYGWIN_RUNTIME=1 |
40 #SMLNJ_CYGWIN_RUNTIME=1 |