src/Tools/WWW_Find/lib/Tools/wwwfind
changeset 43075 6fde0c323c15
parent 37062 2b94e2d406d9
child 51085 d90218288d51
--- a/src/Tools/WWW_Find/lib/Tools/wwwfind	Mon May 30 17:07:48 2011 +0200
+++ b/src/Tools/WWW_Find/lib/Tools/wwwfind	Mon May 30 17:07:48 2011 +0200
@@ -124,7 +124,7 @@
 
 WWWPORT=`sed -e 's/[ 	]*//g' -ne 's/server.port=\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
 SCGIPORT=`sed -e 's/[ 	]*//g' -ne 's/"port"=>\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
-MLSTARTSERVER="ScgiServer.server' 10 \"/\" $SCGIPORT;"
+MLSTARTSERVER="YXML_Find_Theorems.init (); ScgiServer.server' 10 \"/\" $SCGIPORT;"
 
 case "$COMMAND" in
   start)