balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Docs: update links to generated odoc

Browse Source
This commit is contained in:
Benjamin Canou 2018-07-10 15:39:11 +02:00
parent 9f4ff764a8
commit 9ed554f8b2
2 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
docs/_extensions/tezos_custom_roles.py
View File

@ -29,8 +29,8 @@ def package_role(name, rawtext, text, lineno, inliner, options={}, content=[]):
branch = os.environ.get('CI_COMMIT_REF_NAME', 'master') branch = os.environ.get('CI_COMMIT_REF_NAME', 'master')
project_url = os.environ.get('CI_PROJECT_URL', 'https://gitlab.com/tezos/tezos') project_url = os.environ.get('CI_PROJECT_URL', 'https://gitlab.com/tezos/tezos')
src_url = project_url + "/tree/" + branch + "/" + src src_url = project_url + "/tree/" + branch + "/" + src
if os.path.isdir('_build/api/odoc/'+lib): if os.path.isdir('_build/api/odoc/_html/'+lib):
if os.path.isdir(os.path.join('_build','api','odoc',lib,lib.replace('-','_').capitalize())): if os.path.isdir(os.path.join('_build','api','odoc','_html',lib,lib.replace('-','_').capitalize())):
lib = lib + '/' + lib.replace('-','_').capitalize() lib = lib + '/' + lib.replace('-','_').capitalize()
url = "api/api-inline.html#" + lib + '/index.html' url = "api/api-inline.html#" + lib + '/index.html'
for i in range(1,rel_lvl): for i in range(1,rel_lvl):

4
docs/api/api-inline.rst
View File

@ -4,7 +4,7 @@ Online OCaml Documentation
.. raw:: html .. raw:: html
<iframe id="docframe" height="100%" width="100%" src="../api/odoc/index.html"></iframe> <iframe id="docframe" height="100%" width="100%" src="../api/odoc/_html/index.html"></iframe>
<style> <style>
@media (max-width: 771px) { @media (max-width: 771px) {
#docframe { border:none; position: fixed; top: 70px; bottom: 0; right: 0; left: 0; } #docframe { border:none; position: fixed; top: 70px; bottom: 0; right: 0; left: 0; }
@ -15,5 +15,5 @@ Online OCaml Documentation
</style> </style>
<script language="JavaScript"> <script language="JavaScript">
if (window.location.hash.endsWith(".html")) if (window.location.hash.endsWith(".html"))
document.getElementById('docframe').src = "../api/odoc/" + window.location.hash.slice(1) document.getElementById('docframe').src = "../api/odoc/_html/" + window.location.hash.slice(1)
</script> </script>