# HG changeset patch
# User wenzelm
# Date 863454081 -7200
# Node ID c13e54126fcd7dc0506f0af5c0e138f1da3d4b03
# Parent  480bfa3ede7dc21a2c43ffaa8220c90d3a3f4246
improved doc stuff;

diff -r 480bfa3ede7d -r c13e54126fcd Admin/makedist
--- a/Admin/makedist	Mon May 12 17:54:03 1997 +0200
+++ b/Admin/makedist	Mon May 12 18:21:21 1997 +0200
@@ -8,7 +8,6 @@
 ## global settings
 
 LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents TFL Tools ZF"
-DOCS="Intro Ref Logics"
 
 CVSROOT=/isabelle/archive
 DISTBASE=~/tmp/isadist
@@ -105,10 +104,13 @@
 
 # make docs
 
-for D in $DOCS
+cd $DISTBASE/$DISTNAME/Doc
+
+for DOC in $(cat Contents)
 do
-  cd $DISTBASE/$DISTNAME/Doc/$D
+  cd $DOC
   make dist
+  cd ..
 done
 
 
@@ -119,7 +121,7 @@
 find . -name CVS -exec rm -rf {} \;
 
 mkdir -p Tools/8bit/bin    #FIXME tmp
-find Doc -name \*.dvi -exec mv {} Distribution/doc \;
+find Doc -name \*.dvi -o -name \*.eps -o \*.ps -exec mv {} Distribution/doc \;
 rm -rf Admin Doc
 
 mkdir src