diff options
| author | Enrico Tassi | 2017-05-24 10:34:39 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2017-05-24 10:34:39 +0200 |
| commit | 94311c3a8f5ddcf16dce313d3ddf5d7433d57e42 (patch) | |
| tree | 563dd9fce8e7d935c703c34121bcf7b65dd69166 /dev | |
| 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 'dev')
0 files changed, 0 insertions, 0 deletions