1 files changed, 11 insertions, 0 deletions
diff --git a/Makefile b/Makefile
index 754ae3f34..241ec79d0 100644
--- a/Makefile
+++ b/Makefile
@@ -158,11 +158,22 @@ fast-autogenerated-deps: src/Specific/.autgenerated-deps
 	$(SHOW)'CP .v.d'
 	$(HIDE)for i in $(REAL_SPECIFIC_GENERATED_VOFILES:.vo=.v.d); do rm -f $$i; ln -s "$(shell cd src/Specific && pwd)/.autgenerated-deps" $$i; done
 
+.PHONY: fake-autogenerated-deps
+fake-autogenerated-deps:
+	$(SHOW)'FAKE COQDEP SPECIFIC.v.d'
+	$(HIDE)touch $(REAL_SPECIFIC_GENERATED_VOFILES:.vo=.v.d)
+
 ifneq ($(filter fast-autogenerated-deps,$(MAKECMDGOALS)),)
 $(REAL_SPECIFIC_GENERATED_VOFILES:.vo=.v.d): fast-autogenerated-deps
 	@ true
 endif
 
+ifneq ($(filter fake-autogenerated-deps,$(MAKECMDGOALS)),)
+$(REAL_SPECIFIC_GENERATED_VOFILES:.vo=.v.d): fake-autogenerated-deps
+	@ true
+endif
+
+
 printlite::
 	@echo 'Files Made:'
 	@for i in $(sort $(LITE_VOFILES)); do echo $$i; done