[gigatexal]

Yeah that’s my thought as well: this is something GitHub is supposed to do. Keep it simple on the users and leave the hard stuff to the creators/runners of the tool