Admin/makedist
changeset 3169 c13e54126fcd
parent 3099 808681776bf7
child 3186 57be77ca36ff
equal deleted inserted replaced
3168:480bfa3ede7d 3169:c13e54126fcd
     6 
     6 
     7 
     7 
     8 ## global settings
     8 ## global settings
     9 
     9 
    10 LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents TFL Tools ZF"
    10 LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents TFL Tools ZF"
    11 DOCS="Intro Ref Logics"
       
    12 
    11 
    13 CVSROOT=/isabelle/archive
    12 CVSROOT=/isabelle/archive
    14 DISTBASE=~/tmp/isadist
    13 DISTBASE=~/tmp/isadist
    15 
    14 
    16 
    15 
   103 cvs -f -q $EXPORT -P -d $DISTNAME isabelle
   102 cvs -f -q $EXPORT -P -d $DISTNAME isabelle
   104 
   103 
   105 
   104 
   106 # make docs
   105 # make docs
   107 
   106 
   108 for D in $DOCS
   107 cd $DISTBASE/$DISTNAME/Doc
       
   108 
       
   109 for DOC in $(cat Contents)
   109 do
   110 do
   110   cd $DISTBASE/$DISTNAME/Doc/$D
   111   cd $DOC
   111   make dist
   112   make dist
       
   113   cd ..
   112 done
   114 done
   113 
   115 
   114 
   116 
   115 # prepare dist dir for release
   117 # prepare dist dir for release
   116 
   118 
   117 cd $DISTBASE/$DISTNAME
   119 cd $DISTBASE/$DISTNAME
   118 
   120 
   119 find . -name CVS -exec rm -rf {} \;
   121 find . -name CVS -exec rm -rf {} \;
   120 
   122 
   121 mkdir -p Tools/8bit/bin    #FIXME tmp
   123 mkdir -p Tools/8bit/bin    #FIXME tmp
   122 find Doc -name \*.dvi -exec mv {} Distribution/doc \;
   124 find Doc -name \*.dvi -o -name \*.eps -o \*.ps -exec mv {} Distribution/doc \;
   123 rm -rf Admin Doc
   125 rm -rf Admin Doc
   124 
   126 
   125 mkdir src
   127 mkdir src
   126 mv $LOGICS src
   128 mv $LOGICS src
   127 mv index.html src
   129 mv index.html src