diff options
| author | Joachim Breitner | 2018-02-12 10:32:01 -0500 |
|---|---|---|
| committer | Théo Zimmermann | 2018-02-15 10:21:31 +0100 |
| commit | 00dfe2be53ddc84836e095f0a20a0efdebc87f50 (patch) | |
| tree | d2263783fafba64e1eab2af888342e5001f1a8c6 /kernel/type_errors.mli | |
| parent | 52d666a7a83e4023d9f5cd7324ed81c7f7926156 (diff) | |
coq_makefile: Support "" as the prefix in _CoqProject
This fixes #6350 (and even comes with a test case).
Refering to other directories as `-R … ""` is maybe not best practice,
but some people out there do it, so as long as it does not cause too
much trouble, we can continue to support it.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions