diff options
| author | Hugo Herbelin | 2020-10-24 14:44:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-20 20:02:35 +0100 |
| commit | 7508be4f6d61dd2735ff0b8d406a6a66cd2faad9 (patch) | |
| tree | 38c0efea2e171e6f88b074acee52936ae365f4ee /dev/ci/docker | |
| parent | 93654a0ba50f26f90f84e98b33ec13caa92d1799 (diff) | |
Documentation of the support for general single binders in notations.
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
Diffstat (limited to 'dev/ci/docker')
0 files changed, 0 insertions, 0 deletions