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