idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-11 02:01:36 +03:00
Code Issues Projects Releases Wiki Activity

Fix latex rtd generation

Browse Source 
@jfdm tells me that you can only generate one latex document, so let's
make it the tutorial
This commit is contained in:
Edwin Brady 2020-05-20 18:53:56 +01:00
parent 3a915943fc
commit 1fb8904992
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
docs/source/conf.py
View File

@ -162,7 +162,7 @@ latex_elements = {
# (source start file, target name, title,
# author, documentclass [howto, manual, or own class]).
latex_documents = [
('index', 'idris-documentation-complete.tex', u'Documentation for the Idris Language', u'The Idris Community', 'report'),
# ('index', 'idris-documentation-complete.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'),
]