Imported Upstream version 8.3.pl2upstream/8.3.pl2

3 files changed, 98 insertions, 6 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 9bc8965d..3093fa6c 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: coqdep.ml 13983 2011-04-08 17:57:56Z herbelin $ *)
 
 open Printf
 open Coqdep_lexer
@@ -41,8 +41,8 @@ let add_coqlib_known phys_dir log_dir f =
   match get_extension f [".vo"] with
     | (basename,".vo") ->
 	let name = log_dir@[basename] in
-	Hashtbl.add coqlibKnown [basename] ();
-	Hashtbl.add coqlibKnown name ()
+	let paths = suffixes name in
+        List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
 let sort () =
@@ -199,7 +199,8 @@ let coqdep () =
     let coqlib = Envars.coqlib () in
     add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
     add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
-    add_dir add_coqlib_known (coqlib//"user-contrib") []
+    let user = coqlib//"user-contrib" in
+    if Sys.file_exists user then add_rec_dir add_coqlib_known user []
   end;
   List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
   List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu;
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 0961e398..851b7089 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -397,8 +397,7 @@ let rec add_directory recur add_file phys_dir log_dir =
 	  | S_DIR when recur ->
 	      if List.mem phys_f !norecdir_list then ()
 	      else
-		let log_dir' = if log_dir = [] then ["Coq"] else log_dir@[f] in
-		add_directory recur add_file phys_f log_dir'
+		add_directory recur add_file phys_f (log_dir@[f])
 	  | S_REG -> add_file phys_dir log_dir f
 	  | _ -> ()
     done
diff --git a/tools/mkwinapp.ml b/tools/mkwinapp.ml
new file mode 100644
index 00000000..226302fb
--- /dev/null
+++ b/tools/mkwinapp.ml
@@ -0,0 +1,92 @@
+(* OCaml-Win32
+ * mkwinapp.ml
+ * Copyright (c) 2002-2004 by Harry Chomsky
+ *
+ * This library is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU Library General Public
+ * License as published by the Free Software Foundation; either
+ * version 2 of the License, or (at your option) any later version.
+ *
+ * This library is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ * Library General Public License for more details.
+ *
+ * You should have received a copy of the GNU Library General Public
+ * License along with this library; if not, write to the Free
+ * Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+ *)
+
+(*********************************************************************
+ * This program alters an .exe file to make it use the "windows subsystem"
+ * instead of the "console subsystem".  In other words, when Windows runs
+ * the program, it will not create a console for it.
+ *)
+
+(* Pierre Letouzey 23/12/2010 : modification to allow selecting the
+   subsystem to use instead of just setting the windows subsystem *)
+
+(* This tool can be run directly via :
+   ocaml unix.cma mkwinapp.ml [-set|-unset] <filename>
+*)
+
+exception Invalid_file_format
+
+let input_word ic =
+    let lo = input_byte ic in
+    let hi = input_byte ic in
+    (hi lsl 8) + lo
+
+let find_pe_header ic =
+    seek_in ic 0x3C;
+    let peheader = input_word ic in
+    seek_in ic peheader;
+    if input_char ic <> 'P' then
+        raise Invalid_file_format;
+    if input_char ic <> 'E' then
+        raise Invalid_file_format;
+    peheader
+
+let find_optional_header ic =
+    let peheader = find_pe_header ic in
+    let coffheader = peheader + 4 in
+    seek_in ic (coffheader + 16);
+    let optsize = input_word ic in
+    if optsize < 96 then
+        raise Invalid_file_format;
+    let optheader = coffheader + 20 in
+    seek_in ic optheader;
+    let magic = input_word ic in
+    if magic <> 0x010B && magic <> 0x020B then
+        raise Invalid_file_format;
+    optheader
+
+let change flag ic oc =
+    let optheader = find_optional_header ic in
+    seek_out oc (optheader + 64);
+    for i = 1 to 4 do
+        output_byte oc 0
+    done;
+    output_byte oc (if flag then 2 else 3)
+
+let usage () =
+  print_endline "Alters a Win32 executable file to use the Windows subsystem or not.";
+  print_endline "Usage: mkwinapp [-set|-unset] <filename>";
+  print_endline "Giving no option is equivalent to -set";
+  exit 1
+
+let main () =
+  let n = Array.length Sys.argv - 1 in
+  if not (n = 1 || n = 2) then usage ();
+  let flag =
+    if n = 1 then true
+    else if Sys.argv.(1) = "-set" then true
+    else if Sys.argv.(1) = "-unset" then false
+    else usage ()
+  in
+  let filename = Sys.argv.(n) in
+  let f = Unix.openfile filename [Unix.O_RDWR] 0 in
+  let ic = Unix.in_channel_of_descr f and oc = Unix.out_channel_of_descr f in
+  change flag ic oc
+
+let _ = main ()