|
@@ -35,7 +35,7 @@ def RunPager(globalConfig):
|
|
|
return
|
|
return
|
|
|
|
|
|
|
|
if platform_utils.isWindows():
|
|
if platform_utils.isWindows():
|
|
|
- _PipePager(pager);
|
|
|
|
|
|
|
+ _PipePager(pager)
|
|
|
else:
|
|
else:
|
|
|
_ForkPager(pager)
|
|
_ForkPager(pager)
|
|
|
|
|
|
|
@@ -45,7 +45,7 @@ def TerminatePager():
|
|
|
sys.stdout.flush()
|
|
sys.stdout.flush()
|
|
|
sys.stderr.flush()
|
|
sys.stderr.flush()
|
|
|
pager_process.stdin.close()
|
|
pager_process.stdin.close()
|
|
|
- pager_process.wait();
|
|
|
|
|
|
|
+ pager_process.wait()
|
|
|
pager_process = None
|
|
pager_process = None
|
|
|
# Restore initial stdout/err in case there is more output in this process
|
|
# Restore initial stdout/err in case there is more output in this process
|
|
|
# after shutting down the pager process
|
|
# after shutting down the pager process
|