PAL10873: Debian: HOSTNAME settings. A patch by Paul RASCLE.

diff --git a/bin/killSalomeWithPort.py b/bin/killSalomeWithPort.py
index 221ba981e30791ffa5983c48b3f6683bf91f7c8d..bb71dc2f60f69707c21460df58b6870c05a454a3 100755 (executable)
--- a/bin/killSalomeWithPort.py
+++ b/bin/killSalomeWithPort.py
@@ -2,6 +2,14 @@
 import os, sys, pickle, signal, commands
 
 def getPiDict(port,appname='salome',full=True):
+    from Utils_Identity import getShortHostName
+
+    if os.getenv("HOSTNAME") == None:
+        if os.getenv("HOST") == None:
+            os.environ["HOSTNAME"]=getShortHostName()
+        else:
+            os.environ["HOSTNAME"]=os.getenv("HOST")
+
     filedict = []
     filedict.append( os.getenv('USER') )          # user name
     filedict.append( os.getenv('HOSTNAME') )      # host name