Workflow: refrain from using github web ui to merge pull requests
Created by: alive4ever
Hi @ollieparanoid , @MartijnBraam and committers of postmarketOS.
It seems that the workflow to merge pull requests is using github web interface instead of fetching pull requests locally and performs merging process with locally pulled PRs using git command line tool.
I suggest to refrain from using github web interface to merge pull requests and do the merging of pull requests locally for the following reasons:
-
Using the web interface, github will modify the author committer email to username(at)noreply.blablabla, which is probably not desired by pull request submitter. Github also modifies timezone information, which is acquired from github profile instead of timezone used during commit. When merging locally, the author information (including email and timezone) are kept.
-
The main source git repository should be @ollieparanoid's local git repository instead of github repository. Github should only mirror what's in @ollieparanoid local git repository (not vice versa).
-
Locally merging PRs should give flexibility to use the power of git command line tool (interactive rebase, etc).