diff options
| author | Pierre-Marie Pédrot | 2016-01-24 16:25:38 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-24 16:34:02 +0100 |
| commit | f17096fa9eff103f40e6d381ebeb4313002fa378 (patch) | |
| tree | b7eed322565fd51f282872194d688863a70bd4eb /engine | |
| parent | 030ef2f015e5c592ea7599f0f98a715873c1e4d0 (diff) | |
Fixing bug #4373: coqdep does not know about .vio files.
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions