diff options
| author | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
| commit | 8aad36675447f3c95dc2f10e26c4cce48595497b (patch) | |
| tree | deb34d0aebc627d31317ff8ac418f6a07f506632 /plugins | |
| parent | 172708b434ead6c3f824cf51e60c3141597e1e2b (diff) | |
Revert "Fixing printing of pat%constr."
This reverts commit 6f3dc50176fff8b731dcdaf47194f0e3ff21db0c.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions