git.iko.soy/Idris-dev
on master help sign in
Move IDE protocol docs
commit27ccd9a00275a19501f1ff6d5b20fd7c350c0339 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 19 May 2015, 22:05 (11 years ago) parent0a87607
2 files changed+2−9
compare with master
unifiedsplit
docs/index.rst+1−8 docs/ide/protocol.rst → docs/reference/ide-protocol.rst+1−1
docs/index.rst+1−8
@@ -104,6 +104,7 @@ Language Reference
104104 reference/uniqueness-types
105105 reference/ffi
106106 reference/erasure
107+ reference/ide-protocol
107108
108109.. _guides:
109110
@@ -116,11 +117,3 @@ Short Guides
116117
117118 guides/type-providers-ffi
118119
119−############################
120−Implementation Documentation
121−############################
122−
123−.. toctree::
124− :maxdepth: 1
125−
126− ide/protocol
docs/ide/protocol.rst → docs/reference/ide-protocol.rstrenamed+1−1
@@ -1,5 +1,5 @@
11********************
2−Idris's IDE Protocol
2+The IDE Protocol
33********************
44
55The Idris REPL has two modes of interaction: a human-readable syntax designed for direct use in a terminal, and a machine-readable syntax designed for using Idris as a backend for external tools.