From 1fb89049926fdba1354d2c3b8477c0187ff5bbfd Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 20 May 2020 18:53:56 +0100 Subject: [PATCH] Fix latex rtd generation @jfdm tells me that you can only generate one latex document, so let's make it the tutorial --- docs/source/conf.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/conf.py b/docs/source/conf.py index 38d9e9791..29122d6fd 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -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'), ]