eric6/WebBrowser/GreaseMonkey/GreaseMonkeyManager.py

changeset 7836
2f0d208b8137
parent 7785
9978016560ec
child 7923
91e843545d9a
equal deleted inserted replaced
7835:0835ed67714b 7836:2f0d208b8137
128 ) 128 )
129 129
130 if deleteScript: 130 if deleteScript:
131 try: 131 try:
132 os.remove(fileName) 132 os.remove(fileName)
133 except (IOError, OSError): 133 except OSError:
134 # ignore 134 # ignore
135 pass 135 pass
136 136
137 def scriptsDirectory(self): 137 def scriptsDirectory(self):
138 """ 138 """
175 fileName = os.path.join(self.requireScriptsDirectory(), 175 fileName = os.path.join(self.requireScriptsDirectory(),
176 fileName) 176 fileName)
177 try: 177 try:
178 with open(fileName, "r", encoding="utf-8") as f: 178 with open(fileName, "r", encoding="utf-8") as f:
179 source = f.read().strip() 179 source = f.read().strip()
180 except (IOError, OSError): 180 except OSError:
181 source = "" 181 source = ""
182 if source: 182 if source:
183 script += source + "\n" 183 script += source + "\n"
184 184
185 return script 185 return script

eric ide

mercurial