make-dist
author wenzelm
Thu, 26 Feb 1998 10:48:19 +0100
changeset 4655 481628ea8edd
parent 0 a5a9c433f639
permissions -rwxr-xr-x
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
#!/bin/sh
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
#make-dist <DIR> 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
#make a distribution directory of Isabelle sources. Example:    
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
#    rm -r /usr/groups/theory/isabelle/91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
#    make-dist /usr/groups/theory/isabelle/91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
#BEFORE MAKING A NEW DISTRIBUTION VERSION, CHECK...
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
#   * that make-all works perfectly
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
#   * that README files are up-to-date
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
#   * that the version number has been updated
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
#This version copies EVERYTHING!!!!!!!!!!!!!!!!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
set -e		#terminate if error
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
#Pure Isabelle
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
mkdir ${1?'No destination directory specified'}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
cp -ipr . $1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
#TO WRITE POLY/ML AND ISABELLE TAPES, USE SHELL SCRIPT write-dist
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
#TO PACK FOR EMAIL, USE SHELL SCRIPTS make-emaildist, send-emaildist