make-all-nj
author lcp
Wed, 15 Mar 1995 10:56:39 +0100
changeset 955 aa0c5f9daf5b
parent 547 23e30d32cd0d
permissions -rwxr-xr-x
Declares the function exit_use to behave like use but fail if errors are detected. It can be used in all Makefiles except Pure, which will write the exception handler explicitly ("exit" will have been declared already).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
370
e95e212512d1 make-all-poly, make-all-nj: restored to main directory as examples
lcp
parents:
diff changeset
     1
#! /bin/sh
e95e212512d1 make-all-poly, make-all-nj: restored to main directory as examples
lcp
parents:
diff changeset
     2
#Make entire system using Standard ML of New Jersey
e95e212512d1 make-all-poly, make-all-nj: restored to main directory as examples
lcp
parents:
diff changeset
     3
#Pathnames will have to be modified for your site
e95e212512d1 make-all-poly, make-all-nj: restored to main directory as examples
lcp
parents:
diff changeset
     4
ISABELLEBIN=/homes/`whoami`/bin
e95e212512d1 make-all-poly, make-all-nj: restored to main directory as examples
lcp
parents:
diff changeset
     5
ISABELLECOMP=sml
547
23e30d32cd0d deleted obsolete references to ISABELLEMAKE
lcp
parents: 370
diff changeset
     6
export ISABELLEBIN ISABELLECOMP 
370
e95e212512d1 make-all-poly, make-all-nj: restored to main directory as examples
lcp
parents:
diff changeset
     7
nohup make-all $*