25 lines
637 B
Text
25 lines
637 B
Text
Convenience test target
|
|
|
|
Index: Makefile
|
|
--- Makefile.orig
|
|
+++ Makefile
|
|
@@ -229,7 +229,7 @@ runtime:
|
|
|
|
FORCE:
|
|
|
|
-.PHONY: proof extraction runtime FORCE
|
|
+.PHONY: proof extraction runtime test FORCE
|
|
|
|
documentation: $(FILES)
|
|
mkdir -p doc/html
|
|
@@ -341,6 +341,10 @@ ifeq ($(INSTALL_COQDEV),true)
|
|
install -m 0644 ./compcert.config $(DESTDIR)$(COQDEVDIR)
|
|
@(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(DESTDIR)$(COQDEVDIR)/README
|
|
endif
|
|
+
|
|
+test:
|
|
+ env CCOMPOPTS=-Wl,-z,notext $(MAKE) -C test
|
|
+ env CCOMPOPTS=-Wl,-z,notext $(MAKE) -C test test
|
|
|
|
|
|
clean:
|