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