summaryrefslogtreecommitdiff
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /tools/coqdep.ml
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r--tools/coqdep.ml22
1 files changed, 14 insertions, 8 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 6597c3f6..3647152a 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,18 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqdep.ml 8923 2006-06-08 16:39:58Z herbelin $ *)
+(* $Id: coqdep.ml 9276 2006-10-25 13:00:22Z barras $ *)
open Printf
open Coqdep_lexer
open Unix
-let (/) = Filename.concat
-
-let file_concat l =
- if l=[] then "<empty>" else
- List.fold_left (/) (List.hd l) (List.tl l)
-
let stderr = Pervasives.stderr
let stdout = Pervasives.stdout
@@ -28,12 +22,23 @@ let option_D = ref false
let option_w = ref false
let option_i = ref false
let option_sort = ref false
+let option_slash = ref false
let suffixe = ref ".vo"
let suffixe_spec = ref ".vi"
type dir = string option
+(* filename for printing *)
+let (//) s1 s2 =
+ if !option_slash then s1^"/"^s2 else Filename.concat s1 s2
+
+let (/) = Filename.concat
+
+let file_concat l =
+ if l=[] then "<empty>" else
+ List.fold_left (//) (List.hd l) (List.tl l)
+
(* Files specified on the command line *)
let mlAccu = ref ([] : (string * string * dir) list)
and mliAccu = ref ([] : (string * string * dir) list)
@@ -148,7 +153,7 @@ let cut_prefix p s =
if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s
let canonize f = match Sys.os_type with
- | "Win32" -> cut_prefix ".\\" f
+ | "Win32" when not !option_slash -> cut_prefix ".\\" f
| _ -> cut_prefix "./" f
let sort () =
@@ -517,6 +522,7 @@ let coqdep () =
| "-coqlib" :: [] -> usage ()
| "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll
| "-suffix" :: [] -> usage ()
+ | "-slash" :: ll -> option_slash := true; parse ll
| f :: ll -> treat None f; parse ll
| [] -> ()
in