diff options
| author | umarcor <unai.martinezcorral@ehu.eus> | 2020-09-22 04:36:56 +0200 |
|---|---|---|
| committer | tgingold <tgingold@users.noreply.github.com> | 2020-09-22 07:36:33 +0200 |
| commit | f55c4099343832270ee6d3c0f4aa374a72ec9111 (patch) | |
| tree | 1746ee8e442c457f663900c054d528d244f3ae93 /doc | |
| parent | 8d5ae7bf63c616925306b42d42d01d1cebf3ffc7 (diff) | |
| download | ghdl-f55c4099343832270ee6d3c0f4aa374a72ec9111.tar.gz ghdl-f55c4099343832270ee6d3c0f4aa374a72ec9111.tar.bz2 ghdl-f55c4099343832270ee6d3c0f4aa374a72ec9111.zip | |
doc: add gnatdoc HTML output
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/conf.py | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/doc/conf.py b/doc/conf.py index dff335e4d..ced332c9a 100644 --- a/doc/conf.py +++ b/doc/conf.py @@ -113,10 +113,8 @@ if ctx.is_file(): html_theme_path = ["."] html_theme = "_theme" -# Add any paths that contain custom static files (such as style sheets) here, -# relative to this directory. They are copied after the builtin static files, -# so a file named "default.css" will overwrite the builtin "default.css". html_static_path = ['_static'] +html_extra_path = [str(Path(__file__).resolve().parent.parent / 'public')] # Output file base name for HTML help builder. htmlhelp_basename = 'GHDLdoc' |