diff options
| author | Gregory Malecha | 2015-08-11 12:44:29 -0700 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-08-13 17:13:41 +0200 |
| commit | 5cec38e8a2fbe39c75404f249974227afc028f27 (patch) | |
| tree | 468c30c8e2a324ccab70a37e8257d510ce9ba2db /dev | |
| parent | dda6d8f639c912597d5bf9e4f1d8c2c118b8dc48 (diff) | |
report the full module path when reporting errors in coqdep
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions