src/HOL/Tools/Sledgehammer/MaSh/etc/settings

honor externally set MASH_PORT

# -*- shell-script -*- :mode=shellscript:

ISABELLE_SLEDGEHAMMER_MASH="$COMPONENT"

# MASH=yes
if [ -z "$MASH_PORT" ]; then
  MASH_PORT=9255
fi