equal
deleted
inserted
replaced
102 |
102 |
103 cd $DISTBASE |
103 cd $DISTBASE |
104 |
104 |
105 export CVSROOT |
105 export CVSROOT |
106 cvs -f -q $EXPORT -d $DISTNAME isabelle |
106 cvs -f -q $EXPORT -d $DISTNAME isabelle |
|
107 find . -name CVS -exec rm -rf {} \; |
107 |
108 |
108 |
109 |
109 # make docs |
110 # make docs |
110 |
111 |
111 cd $DISTBASE/$DISTNAME/Doc |
112 cd $DISTBASE/$DISTNAME/Doc |
119 |
120 |
120 |
121 |
121 # prepare dist dir for release |
122 # prepare dist dir for release |
122 |
123 |
123 cd $DISTBASE/$DISTNAME |
124 cd $DISTBASE/$DISTNAME |
124 |
|
125 find . -name CVS -exec rm -rf {} \; |
|
126 |
125 |
127 find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) \) \ |
126 find Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) \) \ |
128 -exec mv -f {} Distribution/doc \; |
127 -exec mv -f {} Distribution/doc \; |
129 rm Distribution/doc/Isa-logics.eps |
128 rm Distribution/doc/Isa-logics.eps |
130 cp Admin/index.html $DISTBASE |
129 cp Admin/index.html $DISTBASE |