diff options
| author | Pierre-Marie Pédrot | 2018-05-03 15:06:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-03 15:06:06 +0200 |
| commit | 0793b47d185371cbb389fe45be0691cc984c198c (patch) | |
| tree | 1c1e4312fef645e391572c73475c472ca3624162 /plugins/syntax | |
| parent | fad6eee8ddb28fa7840044c65aa02557285e23f0 (diff) | |
| parent | 880fee8f80503fc8a40e2e07b565cfd2a99d24da (diff) | |
Merge PR #7304: Make `intro`/`intros` progress on existential variables.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions