ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-10-26 18:02:24 +03:00
Code Issues Projects Releases Wiki Activity

Fix Readthedocs PDF generation

Browse Source 
RTD is consistently not building the PDF of the Idris Documentation. I think it is because we have two documents built.
I have made the opinion to only have the main tutorial build, as this would be of most interest to others.
This commit is contained in:
Jan de Muijnck-Hughes 2020-03-10 14:45:05 +00:00
parent b7a191bbf3
commit c76ade1f0a
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
docs/conf.py
View File

@ -301,8 +301,8 @@ latex_elements = {
# (source start file, target name, title,
# author, documentclass [howto, manual, or own class]).
latex_documents = [
(master_doc, 'idris.tex', u'Documentation for the Idris Language', u'The Idris Community', 'report')
, ('tutorial/index', 'idris-tutorial.tex', u'The Idris Tutorial', u'The Idris Community', 'howto'),
# (master_doc, 'idris.tex', u'Documentation for the Idris Language', u'The Idris Community', 'report')
('tutorial/index', 'idris-tutorial.tex', u'The Idris Tutorial', u'The Idris Community', 'howto'),
]