… if that external repo is used anyway, that’s fine
but in this case the build time is hardly worth mentioning - took a few seconds, if even that long
I would not add an external repo for that.
But OP and others might have different priorities, so: thanks for the tip/reminder!