diff -r 3257703e10c5 -r 9978016560ec eric6/WebBrowser/GreaseMonkey/GreaseMonkeyManager.py
--- a/eric6/WebBrowser/GreaseMonkey/GreaseMonkeyManager.py Tue Oct 13 19:02:26 2020 +0200
+++ b/eric6/WebBrowser/GreaseMonkey/GreaseMonkeyManager.py Wed Oct 14 17:50:39 2020 +0200
@@ -175,9 +175,8 @@
fileName = os.path.join(self.requireScriptsDirectory(),
fileName)
try:
- f = open(fileName, "r", encoding="utf-8")
- source = f.read().strip()
- f.close()
+ with open(fileName, "r", encoding="utf-8") as f:
+ source = f.read().strip()
except (IOError, OSError):
source = ""
if source:
