diff options
| author | Hugo Herbelin | 2020-02-14 13:01:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-04 11:56:40 +0100 |
| commit | fb9442de3a7f5cab102f33a342a5fc7f63cd8f1c (patch) | |
| tree | 5d4aa2080df69642bd2121e8c4a2576a2b9cfbb5 /dev/ci | |
| parent | 89f111f2e15d8cab61495a419f0c9f7ae95e086a (diff) | |
Adding support for an "only parsing" modifier in "where"-based notations.
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions