diff options
| author | Pierre-Marie Pédrot | 2013-12-01 17:11:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-12-01 17:14:27 +0100 |
| commit | 233a782a2336f003869f82e697a567ed02885f23 (patch) | |
| tree | 47032c60ff57e6d423f28dc4f2f6b228194a4370 /plugins/xml | |
| parent | e875e90d1d90aec22e6f206f04c4941cb5a3bcd1 (diff) | |
Ensuring the right parsing of glob arguments, used by refine
and instantiate. Each of these tactics uses it at a different
parsing level, thus actually triggering a parsing error after
merging them. This fix implies some code duplication, which is
a pity. The separation between genargs and parsing entries should
be made one day.
Diffstat (limited to 'plugins/xml')
0 files changed, 0 insertions, 0 deletions