diff options
| author | Hugo Herbelin | 2020-02-25 13:53:03 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-28 05:35:56 +0100 |
| commit | a4d8c9414e65271fc97347ae04b0b431206d33f8 (patch) | |
| tree | f9510503c5d2bdde643a4e4121fa793f9a9e6651 /plugins/syntax/float_syntax.ml | |
| parent | 02b40f6cdb7ec56f34c6b773b1d7768b4b135fd9 (diff) | |
Makefile in test-suite: More separation of concerns as suggested by Enrico.
See "https://github.com/coq/coq/pull/10008#discussion_r382899607".
Diffstat (limited to 'plugins/syntax/float_syntax.ml')
0 files changed, 0 insertions, 0 deletions