src/Tools/make-all-nj
changeset 547 23e30d32cd0d
parent 370 e95e212512d1
equal deleted inserted replaced
546:36e40454e03e 547:23e30d32cd0d
     1 #! /bin/sh
     1 #! /bin/sh
     2 #Make entire system using Standard ML of New Jersey
     2 #Make entire system using Standard ML of New Jersey
     3 #Pathnames will have to be modified for your site
     3 #Pathnames will have to be modified for your site
     4 ISABELLEBIN=/homes/`whoami`/bin
     4 ISABELLEBIN=/homes/`whoami`/bin
     5 ISABELLECOMP=sml
     5 ISABELLECOMP=sml
     6 ISABELLEMAKE=Makefile.NJ
     6 export ISABELLEBIN ISABELLECOMP 
     7 export ISABELLEBIN ISABELLECOMP ISABELLEMAKE
       
     8 nohup make-all $*
     7 nohup make-all $*