[ doc ] CHANGELOG + user-manual

This closes #2749
asr · Dec 6, 2017 · c72cd02 · c72cd02
1 parent 058986f
commit c72cd02
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -281,6 +281,12 @@ Pragmas and options
   Attempting to bind `NIL` or `CONS` results in a warning and has otherwise no
   effect.
 
+* The `--no-unicode` pragma prevents Agda from introducing unicode characters
+  when pretty printing a term. Lambda, Arrows and Forall quantifiers are all
+  replaced by their ascii only version. Instead of resorting to subscript
+  suffixes, Agda uses ascii digit characters.
+
+
 Emacs mode
 ----------
 

diff --git a/doc/user-manual/tools/command-line-options.rst b/doc/user-manual/tools/command-line-options.rst
@@ -124,6 +124,8 @@ Printing and debugging
 
 :samp:`--show-irrelevant`                                              Show irrelevant arguments when printing
 
+:samp:`--no-unicode`                                                   Don't use unicode characters to print terms
+
 :samp:`--verbose={N}`                               :samp:`-v={N}`     Set verbosity level to :samp:`{N}`
 ==================================================  =================  ===========================================