Makefile.proof: Also run the regular build as part of proofs
Change-Id: I76eb39e429d3dc540bbcb04ca662c0d15bf7b8a4
Signed-off-by: Nico Huber <nico.h@gmx.de>
Reviewed-on: https://review.sourcearcade.org/c/libhwbase/+/473
Tested-by: Ada SPARK <gnatbot@sourcearcade.org>
Reviewed-by: Angel Pons <th3fanbus@gmail.com>
diff --git a/Makefile.proof b/Makefile.proof
index a08e91c..0332323 100644
--- a/Makefile.proof
+++ b/Makefile.proof
@@ -77,7 +77,7 @@
$(obj)/gnatprove/gnatprove.out: $$($(name)-extra-specs) $$($(name)-extra-gens)
$(obj)/gnatprove/gnatprove.out: $(gpr) $(obj)/proofmode
$(call filter-output, \
- gnatprove -P$< $(SPARKFLAGS) -Xobj=$(abspath $(obj)), \
+ $(MAKE) -j$(jobs) && gnatprove -P$< $(SPARKFLAGS) -Xobj=$(abspath $(obj)), \
sed $(foreach file,$^,-e 's|$(notdir $(file)):[0-9]\+:[0-9]\+:|$(dir $(file))&|'))
proof:
if [ "$(PROOF_MODE)" != "$$(cat $(obj)/proofmode 2>/dev/null)" ]; then \