changeset 7646 | 91a984ba420f |
parent 7645 | cb2459aaa7d7 |
child 7754 | e3da9e7fc584 |
--- a/server/sources/native.py Mon Jul 11 13:23:37 2011 +0200 +++ b/server/sources/native.py Mon Jul 11 13:45:04 2011 +0200 @@ -850,7 +850,9 @@ def _eid_type_source(self, session, eid, sql, _retry=True): try: - return self.doexec(session, sql).fetchone() + res = self.doexec(session, sql).fetchone() + if res is not None: + return res except (self.OperationalError, self.InterfaceError): if session.mode == 'read' and _retry: self.warning("trying to reconnect (eid_type_source())")