diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-05-24 10:34:39 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-05-24 10:34:39 +0200 |
| commit | 94311c3a8f5ddcf16dce313d3ddf5d7433d57e42 (patch) | |
| tree | 563dd9fce8e7d935c703c34121bcf7b65dd69166 /ide | |
| parent | 0ca2fe2e616f303665003bc6cf2d89df385f9394 (diff) | |
coq_makefile: use -include rather than include
This fixes bedrock and eliminates warnings.
Thanks Jason Gross for debugging this!
Diffstat (limited to 'ide')
0 files changed, 0 insertions, 0 deletions