diff options
| author | Pierre-Marie Pédrot | 2014-01-06 19:16:31 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-01-06 20:37:13 +0100 |
| commit | 093529c6d4f8eba7370c30b97d8d648340039374 (patch) | |
| tree | c592d82a5867ee524eebdc1266b0eefa3a11a8ed /dev/base_include | |
| parent | 27d9da372a1c407221e687d9fb0d08fc6fca805f (diff) | |
Adding a -dumpgraph option to Coqdep that output the graph dependency of the
considered files.
Original patch by Guillaume Allais.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions