Admin/makedist
changeset 3099 808681776bf7
parent 3060 7c3564de392e
child 3169 c13e54126fcd
equal deleted inserted replaced
3098:a31170b67367 3099:808681776bf7
    98 echo
    98 echo
    99 
    99 
   100 cd $DISTBASE
   100 cd $DISTBASE
   101 
   101 
   102 export CVSROOT
   102 export CVSROOT
   103 cvs -f -q $EXPORT -d $DISTNAME isabelle
   103 cvs -f -q $EXPORT -P -d $DISTNAME isabelle
   104 
   104 
   105 
   105 
   106 # make docs
   106 # make docs
   107 
   107 
   108 for D in $DOCS
   108 for D in $DOCS
   116 
   116 
   117 cd $DISTBASE/$DISTNAME
   117 cd $DISTBASE/$DISTNAME
   118 
   118 
   119 find . -name CVS -exec rm -rf {} \;
   119 find . -name CVS -exec rm -rf {} \;
   120 
   120 
       
   121 mkdir -p Tools/8bit/bin    #FIXME tmp
   121 find Doc -name \*.dvi -exec mv {} Distribution/doc \;
   122 find Doc -name \*.dvi -exec mv {} Distribution/doc \;
   122 rm -rf Admin Doc examples Modal LK HOLCF/explicit_domains
   123 rm -rf Admin Doc
   123 
   124 
   124 mkdir src
   125 mkdir src
   125 mv $LOGICS src
   126 mv $LOGICS src
   126 mv index.html src
   127 mv index.html src
   127 
   128