diff options
| author | Théo Zimmermann | 2020-11-27 16:22:33 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-27 16:22:41 +0100 |
| commit | 058ac643c5e93da2472e3a0a717b864f49f90b3b (patch) | |
| tree | 12af50d60c3956ef06375eafa26cda87779e8df8 /dev/include | |
| parent | c294664df8e9190a2fbb6153c70c208f58c7db70 (diff) | |
Revert "Remove deprecated tactic cutrewrite."
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions