diff options
| author | Maxime Dénès | 2017-02-16 09:44:48 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-02-16 09:44:48 +0100 |
| commit | bcb634d070519d6e37d9b7d39f12437a7d38f0c2 (patch) | |
| tree | f14702bb8344d82c264966a95f1257d7184df4a7 /tools/coqmktop.ml | |
| parent | ec49fbd7fee9c6ff27f56498a6309d9651b4ef82 (diff) | |
| parent | 888d4be3ea2a45cff416fd8896276cfa8fc00518 (diff) | |
Merge PR#403: Split Vernacular Processing from Toplevel
Diffstat (limited to 'tools/coqmktop.ml')
| -rw-r--r-- | tools/coqmktop.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index eaf938e8ce..645b3665e0 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -75,6 +75,7 @@ let std_includes basedir = let rebase d = match basedir with None -> d | Some base -> base / d in ["-I"; rebase "."; "-I"; rebase "lib"; + "-I"; rebase "vernac"; (* For Mltop *) "-I"; rebase "toplevel"; "-I"; rebase "kernel/byterun"; "-I"; Envars.camlp4lib () ] @ |