Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
make-all-poly
author lcp
Wed, 15 Mar 1995 10:56:39 +0100
changeset 955 aa0c5f9daf5b
parent 699 2da262e85c4d
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
699
2da262e85c4d updated pathnames
lcp
parents: 547
diff changeset 
     2
 
#$Id$
370
e95e212512d1 make-all-poly, make-all-nj: restored to main directory as examples
lcp
parents:
diff changeset 
     3
 
#Make entire system using Poly/ML
e95e212512d1 make-all-poly, make-all-nj: restored to main directory as examples
lcp
parents:
diff changeset 
     4
 
#Pathnames will have to be modified for your site
699
2da262e85c4d updated pathnames
lcp
parents: 547
diff changeset 
     5
 
ML_DBASE=/usr/groups/theory/poly/polyml/`arch`/ML_dbase
2da262e85c4d updated pathnames
lcp
parents: 547
diff changeset 
     6
 
ISABELLEBIN=/homes/`whoami`/dbases
370
e95e212512d1 make-all-poly, make-all-nj: restored to main directory as examples
lcp
parents:
diff changeset 
     7
 
ISABELLECOMP="poly -noDisplay -h 15000"
547
23e30d32cd0d deleted obsolete references to ISABELLEMAKE
lcp
parents: 370
diff changeset 
     8
 
export ML_DBASE ISABELLEBIN ISABELLECOMP
370
e95e212512d1 make-all-poly, make-all-nj: restored to main directory as examples
lcp
parents:
diff changeset 
     9
 
nohup make-all $*
isabelle