Make a new variable, IS_ROB_SERVER, covering behavior of ROBMILES_DEFAULTS and replacing NOT_ROB_SERVER.
I wanted to do this because Rob's server variables can be set in the GitHub workflows (as seen in this commit), while new people setting up Stampy instances would get bit by not setting NOT_ROB_SERVER.
Make a new variable,
IS_ROB_SERVER, covering behavior ofROBMILES_DEFAULTSand replacingNOT_ROB_SERVER.I wanted to do this because Rob's server variables can be set in the GitHub workflows (as seen in this commit), while new people setting up Stampy instances would get bit by not setting
NOT_ROB_SERVER.