# HG changeset patch
# User kleing
# Date 1024602294 -7200
# Node ID c5fad3c40d454a76fdd72df0000eabe61743bf0a
# Parent  a2b09d99e5cfa3a856420b5a0344d23973c7ad4c
fail more gracefully, return proper exit codes, allow preset DISTPREFIX

diff -r a2b09d99e5cf -r c5fad3c40d45 Admin/makedist
--- a/Admin/makedist	Thu Jun 20 18:48:31 2002 +0200
+++ b/Admin/makedist	Thu Jun 20 21:44:54 2002 +0200
@@ -16,12 +16,12 @@
   *broy*)
     export CVSROOT=/usr/proj/isabelle-repository/archive
     ;;
-  *.cl.cam.ac.uk)
-    export CVSROOT=sunbroy2.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/archive
+  *)
+    export CVSROOT=sunbroy2.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/archive       
     ;;
 esac
 
-DISTPREFIX=~/tmp/isadist
+DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
 
 umask 022
 
@@ -116,7 +116,7 @@
 
 cd "$DISTBASE"
 
-$EXPORT
+$EXPORT || fail "Export failed!"
 $FIND . -name CVS -print | xargs rm -rf
 $FIND . -name .cvsignore -print | xargs rm -rf
 $FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
@@ -136,8 +136,8 @@
 for DOC in $(cat Contents)
 do
   cd "$DOC"
-  make dvi
-  [ -n "$PDFLATEX" ] && make clean pdf
+  make dvi || fail "DVI document for $DOC failed!"
+  ([ -n "$PDFLATEX" ] && make clean pdf) || fail "PDF document for $DOC failed!"
   cd ..
 done
 
@@ -148,7 +148,7 @@
 echo "### Preparing distribution ..."
 echo "###"
 
-cd "$DISTBASE/$DISTNAME"
+cd "$DISTBASE/$DISTNAME" || fail "Something is wrong: dist directory doesn't exist!"
 
 cp -R Admin/page ..
 cp Distribution/doc/Contents ../page
@@ -167,7 +167,7 @@
 mv Distribution/* .
 rmdir Distribution
 
-( cd lib/browser; make; )
+( cd lib/browser; make; ) || fail "Graph browser build failed!"
 
 cp doc/isabelle*.eps lib/logo