equal
deleted
inserted
replaced
|
1 #! /bin/sh |
|
2 #Make entire system using Standard ML of New Jersey |
|
3 #Pathnames will have to be modified for your site |
|
4 ISABELLEBIN=/homes/`whoami`/bin |
|
5 ISABELLECOMP=sml |
|
6 ISABELLEMAKE=Makefile.NJ |
|
7 export ISABELLEBIN ISABELLECOMP ISABELLEMAKE |
|
8 nohup make-all $* |