--- a/Admin/makedist Thu Nov 06 10:29:37 1997 +0100
+++ b/Admin/makedist Thu Nov 06 12:27:12 1997 +0100
@@ -121,8 +121,6 @@
find . -name CVS -exec rm -rf {} \;
-( cd Tools/8bit; ./mk; )
-
find Doc \( -name \*.dvi -o -name \*.eps -o -name \*.ps \) -exec mv {} Distribution/doc \;
rm Distribution/doc/Isa-logics.eps
rm -rf Admin Doc
@@ -133,11 +131,8 @@
mv Distribution/* .
rmdir Distribution
-# build theory browser
+( cd lib/browser; make; )
-cd lib/browser
-make
-cd ../..
if [ -n "$UNOFFICIAL" ]; then
{