diff options
| author | Emilio Jesus Gallego Arias | 2018-10-17 14:26:32 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-17 14:41:38 +0200 |
| commit | b33794516f4dd10edcb06be49c0202a9e056c26e (patch) | |
| tree | 0fbf2eff7a667ff5c7f48d3a1c122041a8d26d94 /kernel/make_opcodes.sh | |
| parent | f111af975860b5f48bb792d718e4eb211f6fa57f (diff) | |
[ci] [doc] Notes about branch names.
I'd like to add this convention as it is very convenient for the
development of dev tools. Example, I can do `setup-coq-devs ltac
equations` and then get a fully composed tree. Similarly for preparing
overlays.
Diffstat (limited to 'kernel/make_opcodes.sh')
0 files changed, 0 insertions, 0 deletions