make-dist
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 0 a5a9c433f639
permissions -rwxr-xr-x
made tutorial first;
     1 #!/bin/sh
     2 #make-dist <DIR> 
     3 #make a distribution directory of Isabelle sources. Example:    
     4 #    rm -r /usr/groups/theory/isabelle/91
     5 #    make-dist /usr/groups/theory/isabelle/91
     6 
     7 #BEFORE MAKING A NEW DISTRIBUTION VERSION, CHECK...
     8 #   * that make-all works perfectly
     9 #   * that README files are up-to-date
    10 #   * that the version number has been updated
    11 
    12 #This version copies EVERYTHING!!!!!!!!!!!!!!!!
    13 
    14 set -e		#terminate if error
    15 
    16 #Pure Isabelle
    17 mkdir ${1?'No destination directory specified'}
    18 cp -ipr . $1
    19 
    20 #TO WRITE POLY/ML AND ISABELLE TAPES, USE SHELL SCRIPT write-dist
    21 #TO PACK FOR EMAIL, USE SHELL SCRIPTS make-emaildist, send-emaildist