diff options
| author | Pierre-Marie Pédrot | 2013-11-19 18:31:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-11-19 18:31:39 +0100 |
| commit | 7ca715e5f8a50bca7f5c4eee2c19c94956c59880 (patch) | |
| tree | badd537c17052a63282a57d3e4112db06fc186c2 /dev | |
| parent | 0495194d6040215436ebcc0533b1c05b765e1099 (diff) | |
Optimization: in case of empty substitution, merging is trivial.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions