From 00dcdc88a30adc89065f44fb93a9e6384c217796 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 17 Dec 2008 16:53:39 +0000
Subject: Avoid printing that extraction has created file Foo when it's not the
 case

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11695 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/extract_env.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index e59c5811f6..e2cd2e465f 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -408,7 +408,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
   with e ->
     Option.iter close_out cout; raise e
   end;
-  Option.iter info_file fn;
+  if not dry then Option.iter info_file fn;
   (* Now, let's print the signature *)
   Option.iter
     (fun si ->
-- 
cgit v1.2.3