aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile3
m---------etc/coq-scripts0
2 files changed, 3 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 7a61d0d71..a8f211a5d 100644
--- a/Makefile
+++ b/Makefile
@@ -114,3 +114,6 @@ printenv::
-include etc/coq-scripts/Makefile.vo_closure
printdeps::
$(HIDE)$(foreach vo,$(filter %.vo,$(MAKECMDGOALS)),echo '$(vo): $(call vo_closure,$(vo))'; )
+
+printreversedeps::
+ $(HIDE)$(foreach vo,$(filter %.vo,$(MAKECMDGOALS)),echo '$(vo): $(call vo_reverse_closure,$(vo))'; )
diff --git a/etc/coq-scripts b/etc/coq-scripts
-Subproject 70b32dd2da94b945f4e98064f2fbf78ae0755e6
+Subproject 5c40045ad133614832b9a84eba436c98c93bc58