diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-26 12:14:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-27 21:55:49 +0200 |
| commit | 67335c832a55cbd0ca559906bbe1af2485241353 (patch) | |
| tree | 40ab19e18f8c911b199a574e505eceeaa4e9f95d /tactics/ftactic.mli | |
| parent | 857dc0aaae30805725da213b6550dc1ff3a7adb2 (diff) | |
Revert "Re-add -beautify by default."
This reverts commit 1171590c544492842a848c6765b61c70fca19a01.
Diffstat (limited to 'tactics/ftactic.mli')
0 files changed, 0 insertions, 0 deletions