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 /tools/coq_makefile.ml | |
| 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 'tools/coq_makefile.ml')
| -rw-r--r-- | tools/coq_makefile.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 091869407e..1e1862220b 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -124,7 +124,7 @@ let read_whole_file s = close_in ic; Buffer.contents b -let quote s = if String.contains s ' ' then "'" ^ s ^ "'" else s +let quote s = if String.contains s ' ' || CString.is_empty s then "'" ^ s ^ "'" else s let generate_makefile oc conf_file local_file args project = let makefile_template = |