diff options
| author | Clément Pit-Claudel | 2018-04-29 23:19:39 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2018-05-15 12:05:44 -0400 |
| commit | a68f75ac6bbd26ef1b6e4ccc635f447a48874220 (patch) | |
| tree | 11e53d67172738f5a97d8a61662133da2db38116 /dev/tools | |
| parent | 927b3826e645d428ebe3d8c6599c1f9e2bf79d46 (diff) | |
[doc] Compute the path to coqdoc at run time, not at load time
Diffstat (limited to 'dev/tools')
0 files changed, 0 insertions, 0 deletions