equal
deleted
inserted
replaced
490 |
490 |
491 # SML/NJ |
491 # SML/NJ |
492 |
492 |
493 smlnj_settings = ''' |
493 smlnj_settings = ''' |
494 ML_SYSTEM=smlnj |
494 ML_SYSTEM=smlnj |
495 ML_HOME="/home/smlnj/110.72/bin" |
495 ML_HOME="/home/smlnj/110.74/bin" |
496 ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256" |
496 ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024" |
497 ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") |
497 ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") |
498 ''' |
498 ''' |
499 |
499 |
500 @configuration(repos = [Isabelle], deps = []) |
500 @configuration(repos = [Isabelle], deps = []) |
501 def SML_HOL(*args): |
501 def SML_HOL(*args): |