on master help sign in
Update ide-protocol.rst
e7a4efeAndrei Dziahel
docs/reference/ide-protocol.rst+1−1
@@ -27,7 +27,7 @@ An example interaction from loading the file ``/home/hannes/empty.idr`` looks as
27
27
28The first message is the request from idris-mode to load the specific file, which length is hex 2a, decimal 42 (including the newline at the end).
28The first message is the request from idris-mode to load the specific file, which length is hex 2a, decimal 42 (including the newline at the end).
29The request identifier is set to 1.
29The request identifier is set to 1.
30−The first message from Idris is to write the string ``Type checking /home/hannes/empty.idr'', another is to set the prompt to ``*/home/hannes/empty''.
30+The first message from Idris is to write the string ``Type checking /home/hannes/empty.idr``, another is to set the prompt to ``*/home/hannes/empty``.
31The answer, starting with ``:return`` is ``ok``, and additional information is that the file was loaded.
31The answer, starting with ``:return`` is ``ok``, and additional information is that the file was loaded.
32
32
33There are three atoms in the wire language: numbers, strings, and symbols.
33There are three atoms in the wire language: numbers, strings, and symbols.