diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-26 12:26:48 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-26 12:26:48 +0000 |
| commit | 989171425adc309fbe8021151c9fdd37b9a10d4e (patch) | |
| tree | d6d1d27d2a43ada81b7fa174dd98bf36996a05a9 /tools | |
| parent | 1c4ab025a196d47e20b80f04f60e34edd60a44c2 (diff) | |
Coqdep_boot: one line with bad indentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12018 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdep_boot.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index d259c3be5..b7f6ec250 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -22,7 +22,7 @@ let rec parse = function | "-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 *) - | "-I" :: r :: ll -> + | "-I" :: r :: ll -> (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) add_dir add_known r []; |