diff options
Diffstat (limited to '')
| -rw-r--r-- | Documentation/.gitignore | 1 | ||||
| -rw-r--r-- | Documentation/Makefile | 1 | ||||
| -rw-r--r-- | Documentation/docinfo.html | 5 |
3 files changed, 7 insertions, 0 deletions
diff --git a/Documentation/.gitignore b/Documentation/.gitignore index a48448de32..d11567fbbe 100644 --- a/Documentation/.gitignore +++ b/Documentation/.gitignore @@ -1,5 +1,6 @@ *.xml *.html +!/docinfo.html *.[1-8] *.made *.texi diff --git a/Documentation/Makefile b/Documentation/Makefile index 3f2383a12c..78e407e4bd 100644 --- a/Documentation/Makefile +++ b/Documentation/Makefile @@ -202,6 +202,7 @@ ASCIIDOC_DOCBOOK = docbook5 ASCIIDOC_EXTRA += -acompat-mode -atabsize=8 ASCIIDOC_EXTRA += -I. -rasciidoctor-extensions ASCIIDOC_EXTRA += -alitdd='&\#x2d;&\#x2d;' +ASCIIDOC_EXTRA += -adocinfo=shared ASCIIDOC_DEPS = asciidoctor-extensions.rb GIT-ASCIIDOCFLAGS DBLATEX_COMMON = XMLTO_EXTRA += --skip-validation diff --git a/Documentation/docinfo.html b/Documentation/docinfo.html new file mode 100644 index 0000000000..fb3560eb92 --- /dev/null +++ b/Documentation/docinfo.html @@ -0,0 +1,5 @@ +<style> +pre>code { + display: inline; +} +</style> |