Record TODO.

arthuraa · Jan 22, 2018 · c38c776 · c38c776
1 parent b92e178
commit c38c776
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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.