You can merge an PR always manually via Git. The instructions to do this
are always given in the PR. Look for something like "Merge manually".
Github uses only the normal Git mechanisms.
Oliver
Am 01.10.17 um 23:02 schrieb P. Ottlinger:
Am 30.09.2017 um 23:13 schrieb Anatole Tresch:
I shortly looked at it. It makes sense, so +1 to merge from my side...
I'm unable to accept the PR .... not sure if it's a bug with the
Github-integration, but +1 from me.
Phil
--
N Oliver B. Fischer
A Schönhauser Allee 64, 10437 Berlin, Deutschland/Germany
P +49 30 44793251
M +49 178 7903538
E [email protected]
S oliver.b.fischer
J [email protected]
X http://xing.to/obf
