Admin/makedist
changeset 3638 2b67561c6488
parent 3363 8557c2a1750c
child 3698 0b8986fd9bfc
equal deleted inserted replaced
3637:02ba2acc69c3 3638:2b67561c6488
   131 mv index.html src
   131 mv index.html src
   132 
   132 
   133 mv Distribution/* .
   133 mv Distribution/* .
   134 rmdir Distribution
   134 rmdir Distribution
   135 
   135 
       
   136 # build theory browser
       
   137 
       
   138 cd lib/browser
       
   139 make
       
   140 cd ../..
       
   141 
   136 if [ -n "$UNOFFICIAL" ]; then
   142 if [ -n "$UNOFFICIAL" ]; then
   137   {
   143   {
   138     echo
   144     echo
   139     echo "IMPORTANT NOTE"
   145     echo "IMPORTANT NOTE"
   140     echo "=============="
   146     echo "=============="