diff options
| author |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2013-12-20 16:59:59 +0100 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2013-12-20 17:27:20 +0100 |
| commit | a665fd808b7fdaa11f84b35a87e0b8066cce1eda (patch) | |
| tree | 2b4d5585bdb4b258fdad6f08af5b73bb9408e4a5 /tools/coqdep_boot.ml | |
| parent | ca1305a0187653edcf63e46b84c65130ac78d117 (diff) | |
Coqdep always uses / as dir_sep
Diffstat (limited to 'tools/coqdep_boot.ml')
| -rw-r--r-- | tools/coqdep_boot.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 15fcdc600..588bf2dcf 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -16,7 +16,6 @@ open Coqdep_common *) let rec parse = function - | "-slash" :: ll -> option_slash := true; 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 *) |