# HG changeset patch
# User blanchet
# Date 1380963967 -7200
# Node ID 4a7aa85b6b47cd844ca58b75594cf16260cea737
# Parent  e30e63d05e58958a303711c569b0e3d1f85cc66f
honor externally set MASH_PORT

diff -r e30e63d05e58 -r 4a7aa85b6b47 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