equal
deleted
inserted
replaced
119 |
119 |
120 cd $DISTBASE/$DISTNAME |
120 cd $DISTBASE/$DISTNAME |
121 |
121 |
122 find . -name CVS -exec rm -rf {} \; |
122 find . -name CVS -exec rm -rf {} \; |
123 |
123 |
124 ( cd Tools/8bit; ./mk; ) |
|
125 |
|
126 find Doc \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) -exec mv {} Distribution/doc \; |
124 find Doc \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) -exec mv {} Distribution/doc \; |
127 rm Distribution/doc/Isa-logics.eps |
125 rm Distribution/doc/Isa-logics.eps |
128 rm -rf Admin Doc |
126 rm -rf Admin Doc |
129 |
127 |
130 mkdir src |
128 mkdir src |
131 mv $LOGICS src |
129 mv $LOGICS src |
132 |
130 |
133 mv Distribution/* . |
131 mv Distribution/* . |
134 rmdir Distribution |
132 rmdir Distribution |
135 |
133 |
136 # build theory browser |
134 ( cd lib/browser; make; ) |
137 |
135 |
138 cd lib/browser |
|
139 make |
|
140 cd ../.. |
|
141 |
136 |
142 if [ -n "$UNOFFICIAL" ]; then |
137 if [ -n "$UNOFFICIAL" ]; then |
143 { |
138 { |
144 echo |
139 echo |
145 echo "IMPORTANT NOTE" |
140 echo "IMPORTANT NOTE" |