# HG changeset patch
# User berghofe
# Date 870989968 -7200
# Node ID 2b67561c6488a05dcb31fc92c48c65dcc42bb7e4
# Parent  02ba2acc69c38651c1a5fea9258a66dd78ae21f2
Added some commands for building theory browser.

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