diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-25 23:38:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-25 23:41:48 +0200 |
| commit | 2fa1dc39371b8f770ce662d56d85bf6f20413aac (patch) | |
| tree | cb4686f5ffad055aff805170ff7d6a059a717498 /ide/coq-ssreflect.lang | |
| parent | 1ea09cb57dffd7cc9b6fa3ccec137ea3dfcc6980 (diff) | |
Fix bug #5090: Effect of -Q depends on coqtop's current directory.
This bug was seemingly introduced on purpose by commit 9c5ea63 in 2001. It
seems that the original motivation was to deactivate a warning when overriding
the default loadpath binding of the current directory, but in the end it made
it non-overridable.
Diffstat (limited to 'ide/coq-ssreflect.lang')
0 files changed, 0 insertions, 0 deletions