aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-04-09 12:15:07 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-04-09 12:15:07 -0400
commit6f16c3a8b1b6316e16483f6f916add8d00254628 (patch)
treef0480621f37a842ee80c06a849d201f442b271fb /Makefile
parent399162837dbf57ad18e6e0a8acce67baa132af50 (diff)
Add printreversedeps
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile3
1 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))'; )