From c38c7766b41114ebb8eb2b99518f6983c0a2e0eb Mon Sep 17 00:00:00 2001 From: Arthur Azevedo de Amorim Date: Mon, 22 Jan 2018 11:28:08 -0500 Subject: [PATCH] Record TODO. --- ideas.org | 2 ++ 1 file changed, 2 insertions(+) diff --git a/ideas.org b/ideas.org index b861dd4..cdb5bed 100644 --- a/ideas.org +++ b/ideas.org @@ -16,3 +16,5 @@ ** (Leonidas) Comments in the middle of proofs might make them hard to read. (Antal) It is actually good. ** Get nice output for code that doesn't typecheck. ** Fix paragraphs in MarkDown output. +** Fix GitHub links for text posts. +Right now, only posts with Coq code have GitHub links.