From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 tools/coqdep.ml | 22 ++++++++++++++--------
 1 file changed, 14 insertions(+), 8 deletions(-)

(limited to 'tools/coqdep.ml')

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
-- 
cgit v1.2.3