aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-12-17 21:23:02 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-12-17 21:23:02 +0000
commiteae519a9d8948f353c393ff72bf149e389973edc (patch)
tree3d7f0a40383556ddca65e08e66408d7ed72b5afc
parenta9d3825bf518796bb81e5befa8fb5093855e8e1a (diff)
Coqdep adds %.v.beautified on the left of the ':' when it generates %.v dependecies.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14808 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--tools/coqdep_common.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 45949b924..e412bc8f3 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -404,7 +404,7 @@ let coq_dependencies () =
(fun (name,_) ->
let ename = escape name in
let glob = if !option_noglob then "" else " "^ename^".glob" in
- printf "%s%s%s: %s.v" ename !suffixe glob ename;
+ printf "%s%s%s %s.v.beautified: %s.v" ename !suffixe glob ename ename;
traite_fichier_Coq true (name ^ ".v");
printf "\n";
flush stdout)