aboutsummaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqmktop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 76548aa3d6..9220605e85 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -46,7 +46,7 @@ let camlp4topobjs =
"Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
"Camlp4Parsers/Camlp4OCamlParser.cmo";
"Camlp4Parsers/Camlp4GrammarParser.cmo";
- "q_util.cmo"; "q_coqast.cmo" ]
+ "grammar/q_util.cmo"; "grammar/q_coqast.cmo" ]
let topobjs = camlp4topobjs
let gramobjs = []