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