[webpagereplay] Add command exit.

servermanager.py

Index: servermanager.py
===================================================================
--- servermanager.py	(revision 519)
+++ servermanager.py	(working copy)
@@ -34,6 +34,7 @@
     self.record_callbacks = []
     self.replay_callbacks = []
     self.is_record_mode = is_record_mode
+    self.should_exit = False
 
   def Append(self, initializer, *init_args, **init_kwargs):
     """Append a server to the end of the list to run.
@@ -99,6 +100,8 @@
           server.__enter__()
       while True:
         time.sleep(1)
+        if self.should_exit:

[chrisgao (Use stgao instead), 2013/08/27 16:34:18]

I think we don't need a lock for |should_exit|. It can only be set to True. And
if we miss the updated value, we should not miss it in the next round.

[tonyg, 2013/08/28 01:35:58]

Agreed. Python's GIL takes care of this.

+          break
     except:
       exception_info = sys.exc_info()
     finally: