Show More
@@ -809,7 +809,14 b' class KernelManager(HasTraits):' | |||||
809 | if self._hb_channel is not None: |
|
809 | if self._hb_channel is not None: | |
810 | self._hb_channel.pause() |
|
810 | self._hb_channel.pause() | |
811 |
|
811 | |||
812 | self.kernel.kill() |
|
812 | # Attempt to kill the kernel. | |
|
813 | try: | |||
|
814 | self.kernel.kill() | |||
|
815 | except OSError, e: | |||
|
816 | # In Windows, we will get an Access Denied error if the process | |||
|
817 | # has already terminated. Ignore it. | |||
|
818 | if not (sys.platform == 'win32' and e.winerror == 5): | |||
|
819 | raise | |||
813 | self.kernel = None |
|
820 | self.kernel = None | |
814 | else: |
|
821 | else: | |
815 | raise RuntimeError("Cannot kill kernel. No kernel is running!") |
|
822 | raise RuntimeError("Cannot kill kernel. No kernel is running!") |
General Comments 0
You need to be logged in to leave comments.
Login now