diff options
| author | Pierre-Marie Pédrot | 2021-04-06 13:15:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-04-06 13:15:58 +0200 |
| commit | eb5eb561ccac73ea1f4dc998fe1331405e3820cb (patch) | |
| tree | b55a4ece25d57e12352ace7f8f400218a73dd575 /dev/header.py | |
| parent | e00020734c97242d61008a049f8d1e1344afe31d (diff) | |
| parent | 3031dc74aa4b42e83dba4e1a97ad4c520731cc14 (diff) | |
Merge PR #14063: Coqide: fixes #10720, highlight Variant keyword
Diffstat (limited to 'dev/header.py')
0 files changed, 0 insertions, 0 deletions