Closed mtzguido closed 5 years ago
Github let me merge via the web UI... but I was getting this from my computer:
remote: error: GH006: Protected branch update failed for refs/heads/master.
remote: error: Required status check "license/cla" is expected.
To github.com:mitls/mitls-fstar.git
! [remote rejected] master -> master (protected branch hook declined)
error: failed to push some refs to 'git@github.com:mitls/mitls-fstar.git'
Anyway, sorry for the noise.
Apparently I need to accept the CLA, since I can't push manually, so making this PR