2 Commits

Author	SHA1	Message	Date
Mike Fährmann	4d6ec6958d	[scripts] add 'push --force' to pull-request	2024-01-15 22:37:33 +01:00
Mike Fährmann	f0b76e0bb5	publish pull request helper script ... it's what I've been using to manage GitHub pull requests locally	2023-05-04 10:46:38 +02:00