server/serverctl.py
changeset 1251 af40e615dc89
parent 136 ff51a18c66a3
child 1263 01152fffd593
equal deleted inserted replaced
1250:5c20a7f13c84 1251:af40e615dc89
   473     print cmd
   473     print cmd
   474     if os.system(cmd):
   474     if os.system(cmd):
   475         raise ExecutionError('Error while retrieving the dump')
   475         raise ExecutionError('Error while retrieving the dump')
   476     rmcmd = 'ssh -t %s "rm -f /tmp/%s.dump"' % (host, appid)
   476     rmcmd = 'ssh -t %s "rm -f /tmp/%s.dump"' % (host, appid)
   477     print rmcmd
   477     print rmcmd
   478     if os.system(rmcmd) and not confirm('an error occured while deleting remote dump. Continue anyway?'):
   478     if os.system(rmcmd) and not confirm(
       
   479         'an error occured while deleting remote dump. Continue anyway?'):
   479         raise ExecutionError('Error while deleting remote dump')
   480         raise ExecutionError('Error while deleting remote dump')
   480 
   481 
   481 def _local_dump(appid, output):
   482 def _local_dump(appid, output):
   482     config = ServerConfiguration.config_for(appid)
   483     config = ServerConfiguration.config_for(appid)
   483     # schema=1 to avoid unnecessary schema loading
   484     # schema=1 to avoid unnecessary schema loading