28 lines
702 B
Plaintext
28 lines
702 B
Plaintext
$OpenBSD: patch-Makefile,v 1.9 2021/02/13 17:46:38 daniel Exp $
|
|
|
|
Convenience test target
|
|
|
|
Index: Makefile
|
|
--- Makefile.orig
|
|
+++ Makefile
|
|
@@ -212,7 +212,7 @@ runtime:
|
|
|
|
FORCE:
|
|
|
|
-.PHONY: proof extraction runtime FORCE
|
|
+.PHONY: proof extraction runtime test FORCE
|
|
|
|
documentation: $(FILES)
|
|
mkdir -p doc/html
|
|
@@ -319,6 +319,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:
|