make-dist
author wenzelm
Thu, 20 Nov 1997 12:49:25 +0100
changeset 4248 5e8a31c41d44
parent 0 a5a9c433f639
permissions -rwxr-xr-x
added get_error: 'a error -> string option, get_ok: 'a error -> 'a option; added multiply: 'a list * 'a list list -> 'a list list;

#!/bin/sh
#make-dist <DIR> 
#make a distribution directory of Isabelle sources. Example:    
#    rm -r /usr/groups/theory/isabelle/91
#    make-dist /usr/groups/theory/isabelle/91

#BEFORE MAKING A NEW DISTRIBUTION VERSION, CHECK...
#   * that make-all works perfectly
#   * that README files are up-to-date
#   * that the version number has been updated

#This version copies EVERYTHING!!!!!!!!!!!!!!!!

set -e		#terminate if error

#Pure Isabelle
mkdir ${1?'No destination directory specified'}
cp -ipr . $1

#TO WRITE POLY/ML AND ISABELLE TAPES, USE SHELL SCRIPT write-dist
#TO PACK FOR EMAIL, USE SHELL SCRIPTS make-emaildist, send-emaildist