Am Do., 5. Dez. 2019 um 15:22 Uhr schrieb Jorge Fernandez Monteagudo <jorgefm@cirsa.com>:

One noob question. Can I push a change from a commit (f77f2c79c2bb898c123ffe89a0bd1acb5362afc5)
not the master? From this commit I can make it boot but from the last there are
a lot of changes to made...

You can, yes. If it can't be merged, that's only for review, but it would be a start.

Patrick

Google Germany GmbH, ABC-Str. 19, 20354 Hamburg
Registergericht und -nummer: Hamburg, HRB 86891, Sitz der Gesellschaft: Hamburg
Geschäftsführer: Paul Manicle, Halimah DeLaine Prado