Re: [GHC] #15538: GHC boot script can't handle Git remote not named origin (was: GHC boot script can't handle Git origin not named origin)