diff -r 02ba2acc69c3 -r 2b67561c6488 Admin/makedist
--- a/Admin/makedist	Thu Aug 07 23:37:53 1997 +0200
+++ b/Admin/makedist	Thu Aug 07 23:39:28 1997 +0200
@@ -133,6 +133,12 @@
 mv Distribution/* .
 rmdir Distribution
 
+# build theory browser
+
+cd lib/browser
+make
+cd ../..
+
 if [ -n "$UNOFFICIAL" ]; then
   {
     echo