--- a/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py Thu Sep 12 00:34:48 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py Thu Sep 12 09:59:45 2013 +0200
@@ -41,7 +41,7 @@
path = dirname(realpath(__file__))
spawnDaemon(os.path.join(path,'server.py'))
serverIsUp=False
- for _i in range(10):
+ for _i in range(20):
# Test if server is up
try:
sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
@@ -118,11 +118,12 @@
OS.write('%s\n' % received)
OS.close()
IS.close()
+
+ # Statistics
+ if args.statistics:
+ received = communicate('avgStats',args.host,args.port)
+ logger.info(received)
- # Statistics
- if args.statistics:
- received = communicate('avgStats',args.host,args.port)
- logger.info(received)
if args.saveModels:
communicate('save',args.host,args.port)