equal
deleted
inserted
replaced
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 $* |