diff options
| author | Hugo Herbelin | 2016-07-17 13:26:13 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-07-17 14:27:18 +0200 |
| commit | a622696bbe5c6752e49dabb4d3740acf113080ee (patch) | |
| tree | c556bcef3405b85cb2ae858752fa37f61a5883ae /plugins | |
| parent | b976aa1e49579b7b50cfb140cbac8cb6f4c881a7 (diff) | |
Partial fix to #4592 (notation requiring alpha-conversion for printing).
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions