diff options
| author | Gaëtan Gilbert | 2020-11-11 21:08:15 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-12 10:26:42 +0100 |
| commit | 18db1c084c969c898c7fb5aaee101f406d38da4d (patch) | |
| tree | aa487f0361b2136ef919644b72ed4345db12f314 /doc/plugin_tutorial/tuto3/_CoqProject | |
| parent | af42e1bec2df12355725bc79e2060f5d3acd0ce1 (diff) | |
Fix Iris CI script
Also add nice error message when the grep produces an empty result
Diffstat (limited to 'doc/plugin_tutorial/tuto3/_CoqProject')
0 files changed, 0 insertions, 0 deletions