diff options
| author | Gaëtan Gilbert | 2019-01-07 14:08:59 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-08 16:41:11 +0100 |
| commit | 748d1d957b4f866cdb10671f4383be05a1105d06 (patch) | |
| tree | 0f5f19804f2dc88306a51056f04156d3bb0c2f11 /doc/plugin_tutorial/Makefile | |
| parent | fde557d9e92d2ddd3c79d8a620f2cb33ce64a49f (diff) | |
Fix undefined variables in coq_makefile
Detected by running plugin_tutorial from the main makefile which has
--warn-undefined-variables on.
Diffstat (limited to 'doc/plugin_tutorial/Makefile')
0 files changed, 0 insertions, 0 deletions