aboutsummaryrefslogtreecommitdiffhomepage
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 cd6a5078a..a787b1e78 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -100,7 +100,7 @@ let files_to_link userfiles =
let toplevel_objs =
if !top then topobjs else if !opt then notopobjs else [] in
let ide_objs = if !coqide then
- "threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide
+ "str.cma"::"threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide
else []
in
let objs =