equal
deleted
inserted
replaced
322 |
322 |
323 # SML/NJ |
323 # SML/NJ |
324 |
324 |
325 smlnj_settings = ''' |
325 smlnj_settings = ''' |
326 ML_SYSTEM=smlnj |
326 ML_SYSTEM=smlnj |
327 ML_HOME="/home/smlnj/110.74/bin" |
327 ML_HOME="/home/smlnj/110.76/bin" |
328 ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024" |
328 ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024" |
329 ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") |
329 ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") |
330 ''' |
330 ''' |
331 |
331 |
332 @configuration(repos = [Isabelle], deps = [(Pure, [0])]) |
332 @configuration(repos = [Isabelle], deps = [(Pure, [0])]) |