honor externally set MASH_PORT
authorblanchet
Sat, 05 Oct 2013 11:06:07 +0200
changeset 54066 4a7aa85b6b47
parent 54065 e30e63d05e58
child 54067 7be49e2bfccc
honor externally set MASH_PORT
src/HOL/Tools/Sledgehammer/MaSh/etc/settings
--- a/src/HOL/Tools/Sledgehammer/MaSh/etc/settings	Fri Oct 04 18:27:07 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/etc/settings	Sat Oct 05 11:06:07 2013 +0200
@@ -3,4 +3,6 @@
 ISABELLE_SLEDGEHAMMER_MASH="$COMPONENT"
 
 # MASH=yes
-MASH_PORT=9255
+if [ -z "$MASH_PORT" ]; then
+  MASH_PORT=9255
+fi