diff options
| author | Jason Gross | 2020-05-09 13:39:34 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-09 13:39:34 -0400 |
| commit | 6b223d1d668ecb76aa2609b7d6bb8a19e13136cd (patch) | |
| tree | 8e67bb69a5b1bf7371c9e80adb75096e0077b03d /Makefile.dev | |
| parent | 3c66c60e52b334482bcfe3d1d97bb77e4d011d18 (diff) | |
Revert "[with_strategy] Fix for coqchk"
This reverts commit 3c66c60e52b334482bcfe3d1d97bb77e4d011d18.
We instead add a warning in the manual and a kludge in the test-suite.
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions