diff options
Diffstat (limited to 'scripts')
| -rw-r--r-- | scripts/coqmktop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 936e159dea..bd21c1c52d 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -285,7 +285,7 @@ let main () = (*file for dynlink *) let dynlink= if not (!opt || !top) then - [(print_int 2; tmp_dynlink())] + [tmp_dynlink()] else [] in |