diff options
Diffstat (limited to 'doc/refman/RefMan-syn.tex')
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 548c25985..6b471ec39 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -1101,8 +1101,6 @@ places where a list of the underlying entry can be used: {\nterm{entry}} is either {\tt\small constr}, {\tt\small hyp}, {\tt\small integer} or {\tt\small int\_or\_var}. -% $Id$ - %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" |