diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-02 22:08:30 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-02 22:08:30 +0000 |
| commit | 5635c35ea4ec172fd81147effed4f33e2f581aaa (patch) | |
| tree | 303bb7d5a991cef2edbd4899e50a10b47d39e1b5 /plugins/xml | |
| parent | 42cbb18f5b0e220a832ccf5db320d90be5ce0c8e (diff) | |
Mod_subst.force: avoid using join when only one subst
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16381 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml')
0 files changed, 0 insertions, 0 deletions