From f01bf5798224e83b120ac5e3b251514e8cf6bea3 Mon Sep 17 00:00:00 2001 From: =?utf8?q?C=C3=A9dric=20Aguerre?= Date: Wed, 29 Jul 2015 09:36:56 +0200 Subject: [PATCH] Remove ports from PortManager config file if unused --- bin/killSalomeWithPort.py | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/bin/killSalomeWithPort.py b/bin/killSalomeWithPort.py index c340e4863..d973eae00 100755 --- a/bin/killSalomeWithPort.py +++ b/bin/killSalomeWithPort.py @@ -374,6 +374,16 @@ def killMyPort(port): import PortManager # do not remove! Test for PortManager availability! filedict = getPiDict(port) if not os.path.isfile(filedict): # removed by previous call, see (1) + if verbose(): + print "SALOME on port %s: already removed by previous call"%port + # Remove port from PortManager config file + try: + from PortManager import releasePort + if verbose(): + print "Removing port from PortManager configuration file" + releasePort(port) + except ImportError: + pass return except: pass -- 2.39.2