--- 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