Skip to content

Commit 863008d

Browse files
committed
Make path transformation more robust and support deeply nested HTML files.
1 parent f1c2a76 commit 863008d

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

src/Makefile

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,10 @@ all: $(FILES_HTML)
1313
%.html: %.v %.glob jscoqdoc
1414
./jscoqdoc $<
1515
mv $(<F:.v=.html) $@
16-
sed -i 's/\.\//\.\.\//' $@
16+
DIRNAME=$$(dirname $@ | sed 's|^\./||;s|/*$$||') ; \
17+
DEPTH=$$(echo "$$DIRNAME" | awk -F/ '{if ($$1=="") print 0; else print NF}') ; \
18+
PREFIX=$$(printf '../%.0s' $$(seq 1 $$DEPTH)) ; \
19+
sed -i -E "s#(src|href)=\"\./#\1=\"$${PREFIX}#g" $@
1720

1821
%.glob: %.v
1922
coqc $<

0 commit comments

Comments
 (0)