diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-29 14:49:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-29 14:51:53 +0100 |
| commit | a4dce1658f9a946cedb40ddcf0cdbc5391dd2005 (patch) | |
| tree | c20ba51c0b1d83466e235c8ef75d337dd59b919b /man | |
| parent | 8ddc9cbd13ffc22a5895560102852506c9b1ece3 (diff) | |
Forbid implicitly relative names in the checker.
Before this patch, passing a mere identifier (without dots) to the checker
would make it consider it as implicitly referring to a relative name. For
instance, if passed "foo", it would have looked for "Bar.foo.vo" and
"Qux.foo.vo" if those files were in the loadpath.
This was quite ad-hoc. We remove this "feature" and require the user to
always give either a filename or a fully qualified logical name.
Diffstat (limited to 'man')
0 files changed, 0 insertions, 0 deletions