diff options
| author | Pierre-Marie Pédrot | 2016-09-25 23:38:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-25 23:41:48 +0200 |
| commit | 2fa1dc39371b8f770ce662d56d85bf6f20413aac (patch) | |
| tree | cb4686f5ffad055aff805170ff7d6a059a717498 /kernel/nativelambda.mli | |
| 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 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions