diff --git a/doc/.gitignore b/doc/.gitignore new file mode 100644 index 0000000..5ccff1a --- /dev/null +++ b/doc/.gitignore @@ -0,0 +1 @@ +html/ diff --git a/doc/Makefile b/doc/Makefile new file mode 100644 index 0000000..d5a37da --- /dev/null +++ b/doc/Makefile @@ -0,0 +1,16 @@ +.PHONY: all clean + +all: html/abi.html html/il.html + +clean: + rm -fr html + +html/%.html: %.txt + mkdir html 2> /dev/null || true + ( echo ""; \ + echo ""; \ + echo '