diff options
| author | Maxime Dénès | 2017-12-11 15:56:12 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-11 15:56:12 +0100 |
| commit | 4cd5ba6019ecf8a9c41c8594a5446286af725793 (patch) | |
| tree | 52555a6f72d481085151d117973db30924487991 /dev/doc | |
| parent | ecf15647873e390171d6a62f9c28162424cb5a65 (diff) | |
| parent | 511d3ed44705c58234b95b65500f9f597d56c7cf (diff) | |
Merge PR #6311: Don't Add LoadPath on CoqIDE startup, #6153
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions