git.iko.soy/Idris-dev
on master help sign in
Fix Readthedocs PDF generation

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.

commitc76ade1f0a6aef9cf9984fec475b935794715957 authorJan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk> dateTue 10 Mar 2020, 14:45 (7 years ago) parentb7a191b
1 file changed+2−2
compare with master
unifiedsplit
docs/conf.py+2−2
docs/conf.py+2−2
@@ -301,8 +301,8 @@ latex_elements = {
301301# (source start file, target name, title,
302302# author, documentclass [howto, manual, or own class]).
303303latex_documents = [
304− (master_doc, 'idris.tex', u'Documentation for the Idris Language', u'The Idris Community', 'report')
305− , ('tutorial/index', 'idris-tutorial.tex', u'The Idris Tutorial', u'The Idris Community', 'howto'),
304+ # (master_doc, 'idris.tex', u'Documentation for the Idris Language', u'The Idris Community', 'report')
305+ ('tutorial/index', 'idris-tutorial.tex', u'The Idris Tutorial', u'The Idris Community', 'howto'),
306306]
307307
308308