diff options
| author | Gaëtan Gilbert | 2019-03-01 14:23:29 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-01 14:23:29 +0100 |
| commit | e0961f413c5c1ef9418bd86a517704b1dd1f063f (patch) | |
| tree | e4892566b261522ab7fcbcf3d0130c2c26f2b66a /doc/plugin_tutorial/Makefile | |
| parent | ed5685a2afaa9c429d1f16950317363d9b0bc1a8 (diff) | |
Update coqdev.el to use -topfile
PG would do it by default but since we override coq-prog-args it
doesn't.
Diffstat (limited to 'doc/plugin_tutorial/Makefile')
0 files changed, 0 insertions, 0 deletions