diff options
| author | Pierre Courtieu | 2020-10-16 09:14:11 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2020-10-16 17:31:52 +0200 |
| commit | 0fdb1ae633baeb9afb07bbd8632bece5976f95f2 (patch) | |
| tree | 1b65c8a70729ab6132a7cd8c9215a2ec4e40cab7 /generic | |
| parent | eb6bba151b27f4d821088e10e1bda5cad0b70a28 (diff) | |
Fix #514 + support for named goal selector.
It was hard to separate this too fixes (same regexps).
Diffstat (limited to 'generic')
0 files changed, 0 insertions, 0 deletions