diff options
| -rw-r--r-- | pager.py | 4 |
1 files changed, 2 insertions, 2 deletions
| @@ -35,7 +35,7 @@ def RunPager(globalConfig): | |||
| 35 | return | 35 | return |
| 36 | 36 | ||
| 37 | if platform_utils.isWindows(): | 37 | if platform_utils.isWindows(): |
| 38 | _PipePager(pager); | 38 | _PipePager(pager) |
| 39 | else: | 39 | else: |
| 40 | _ForkPager(pager) | 40 | _ForkPager(pager) |
| 41 | 41 | ||
| @@ -45,7 +45,7 @@ def TerminatePager(): | |||
| 45 | sys.stdout.flush() | 45 | sys.stdout.flush() |
| 46 | sys.stderr.flush() | 46 | sys.stderr.flush() |
| 47 | pager_process.stdin.close() | 47 | pager_process.stdin.close() |
| 48 | pager_process.wait(); | 48 | pager_process.wait() |
| 49 | pager_process = None | 49 | pager_process = None |
| 50 | # Restore initial stdout/err in case there is more output in this process | 50 | # Restore initial stdout/err in case there is more output in this process |
| 51 | # after shutting down the pager process | 51 | # after shutting down the pager process |
