diff options
author | 2018-03-22 17:28:13 +0100 | |
---|---|---|
committer | 2018-03-23 15:37:32 +0100 | |
commit | ee62b9269beb78b12f1431816ea1acc0cd09130c (patch) | |
tree | d135a89029348aef2bb2537ba971381fae2d6748 /test-suite/coq-makefile/mlpack1 | |
parent | d275cbc0980ecca00c6a8e0ed172df67eef3d8f4 (diff) |
More precise wording about the merge process.
In particular, don't use the GitHub interface. Also, not all reviews are
mandatory in some corner cases.
Diffstat (limited to 'test-suite/coq-makefile/mlpack1')
0 files changed, 0 insertions, 0 deletions