aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_boot.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdep_boot.ml')
-rw-r--r--tools/coqdep_boot.ml6
1 files changed, 1 insertions, 5 deletions
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 25f62d2be..6fc826833 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -16,11 +16,7 @@ open Coqdep_common
*)
let rec parse = function
- | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll
- | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll
- | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll
- | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll
- | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll
+ | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll
| "-c" :: ll -> option_c := true; parse ll
| "-boot" :: ll -> parse ll (* We're already in boot mode by default *)
| "-mldep" :: ocamldep :: ll ->