mirror of https://github.com/OpenIdentityPlatform/OpenDJ.git
opends/src/server/org/opends/server/replication/server/DbHandler.java @@ -340,6 +340,8 @@ flush(); db.shutdown(); DirectoryServer.deregisterMonitorProvider( dbMonitor.getMonitorInstanceName()); } /**