commit: 10510e60c2f5b5e3a3cc9c54d5a8d38ea6288b1a
Author: Ulrich Müller <ulm <AT> gentoo <DOT> org>
AuthorDate: Tue Jun 11 16:17:59 2024 +0000
Commit: Ulrich Müller <ulm <AT> gentoo <DOT> org>
CommitDate: Tue Jun 11 16:17:59 2024 +0000
URL: https://gitweb.gentoo.org/proj/devmanual.git/commit/?id=10510e60
Makefile: Check if /guide/@self agrees with the document path
Signed-off-by: Ulrich Müller <ulm <AT> gentoo.org>
Makefile | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/Makefile b/Makefile
index 1bfa86e..8f3014e 100644
--- a/Makefile
+++ b/Makefile
@@ -89,6 +89,13 @@ install: all
validate: devbook.rng
@xmllint --noout --quiet --relaxng $< $(XMLS)
+ @# Check if /guide/@self agrees with the document path
+ @for file in $(XMLS); do \
+ self=$$(xmllint --quiet --xpath 'string(/guide/@self)' $${file}); \
+ if test "$${self}text.xml" != "$${file#./}"; then \
+ echo "$${file}: bad self attribute '$${self}'"; exit 1; \
+ fi; \
+ done
@echo "xmllint validation successful"
%.rng: %.rnc
