# HG changeset patch
# User wenzelm
# Date 933192118 -7200
# Node ID fdb397af4cabf947f9cf5178a38d03dfb820fae7
# Parent  df7cf6e8550164ea8d89df6c6b4450a879c00ace
ML_HOME=$ISABELLE_HOME/../smlnj/bin;

diff -r df7cf6e85501 -r fdb397af4cab etc/settings
--- a/etc/settings	Wed Jul 28 19:14:33 1999 +0200
+++ b/etc/settings	Wed Jul 28 22:01:58 1999 +0200
@@ -13,7 +13,7 @@
 
 # Standard ML of New Jersey 110 or later
 ML_SYSTEM=smlnj-110
-ML_HOME=/usr/share/smlnj/bin
+ML_HOME=$ISABELLE_HOME/../smlnj/bin
 ML_OPTIONS="@SMLdebug=/dev/null"
 ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX)