Set Default Goal Selector
As a follow-up to !491 (merged), @tchajed suggested to add
Set Default Goal Selector "!".
To enforce that we properly use goal selectors.
As a follow-up to !491 (merged), @tchajed suggested to add
Set Default Goal Selector "!".
To enforce that we properly use goal selectors.