blob: d9fc684254aa19f6ccec28eccba787d55a27b203 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
--- src/gen_dispatch.py.orig 2020-09-30 06:33:23.765680489 +0200
+++ src/gen_dispatch.py 2020-09-30 06:37:07.719152050 +0200
@@ -182,6 +182,10 @@
# provided the name of the symbol to be requested.
self.provider_loader = {}
+ def __del__(self):
+ if self.out_file is not None:
+ close(self.out_file)
+
def all_text_until_element_name(self, element, element_name):
text = ''
|
