Commit 2cbe23b1 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add a Makefile rule to detect obsolete edited proofs in examples.

parent 50216dec
......@@ -2120,6 +2120,16 @@ clean::
$(foreach d,$(CLEANDIRS),rm -f $(addprefix $(d)/*.,$(COMPILED_LIB_EXTS));)
$(foreach p,$(CLEANLIBS),rm -f $(addprefix $(p).,$(COMPILED_LIB_EXTS));)
detect-unused:
@L1=$$(mktemp); \
L2=$$(mktemp); \
for d in `find examples/ -name 'why3session.xml' -printf '%h\n'`; do \
sed -n -e 's/.*edited="\([^"]*\)".*/\1/p' $$d/why3session.xml | sort > $$L1; \
(cd $$d; git ls-files) | grep -v -e '^why3session.xml' -e '^why3shapes' -e '^[.]gitignore' -e '^Makefile' -e '[.]ml$$' -e '[.]html$$' | sed -e 's/[.]prf$$/.pvs/;s/[.]thy$$/.xml/' | sort -u > $$L2; \
diff -u --label="$$d/why3session.xml" --label="$$d/" $$L1 $$L2 || echo; \
done; \
rm $$L1 $$L2
##################################################################
# Building the Why3 platform with ocamlbuild (OCaml 3.10 needed) #
##################################################################
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment