diff options
author | 2017-03-23 20:12:57 +0100 | |
---|---|---|
committer | 2017-03-23 20:12:57 +0100 | |
commit | 62ce0d1ec197d70a81faf12e151a3da618b2d1ba (patch) | |
tree | fab23723694bc14cbf775a0bc6791df08083645c /doc | |
parent | 530cd175c1b7465c3fa35c300f42b022bed9b25b (diff) | |
parent | 347827ef4ea72048762c1677f37cb716109a5d9c (diff) |
Merge PR#433: doc: fix a French-ism
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-syn.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 61093709e..ecaf82806 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -120,7 +120,7 @@ Notation "A \/ B" := (or A B) (at level 85, right associativity). By default, a notation is considered non associative, but the precedence level is mandatory (except for special cases whose level is -canonical). The level is either a number or the mention {\tt next +canonical). The level is either a number or the phrase {\tt next level} whose meaning is obvious. The list of levels already assigned is on Figure~\ref{init-notations}. |