devtools/__init__.py
changeset 10819 5b5864483c4d
parent 10796 26a36c2a5fbd
child 10888 fbbb028d0a75
--- a/devtools/__init__.py	Mon Oct 19 17:53:51 2015 +0200
+++ b/devtools/__init__.py	Mon Oct 19 17:54:26 2015 +0200
@@ -370,7 +370,8 @@
         # XXX set a clearer error message ???
         backup_coordinates, config_path = self.db_cache[self.db_cache_key(db_id)]
         # reload the config used to create the database.
-        config = pickle.loads(open(config_path, 'rb').read())
+        with open(config_path, 'rb') as f:
+            config = pickle.load(f)
         # shutdown repo before changing database content
         if self._repo is not None:
             self._repo.turn_repo_off()