empire/empserver
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

doc/xdump: Fix definition of identifier in grammar

Browse source 
getid() requires identifiers to start with a letter.  Fix the
documentation to match the code.

Signed-off-by: Markus Armbruster <armbru@pond.sub.org>
This commit is contained in:
Markus Armbruster 2016-06-13 21:58:49 +02:00
parent cc61904354
commit 6316072508
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
doc/xdump
View file

@ -173,7 +173,8 @@ use '-' in meta-identifiers and omit the concatenation symbol ','.
table = header { record } footer ; table = header { record } footer ;
header = "XDUMP" space [ "meta" space ] header = "XDUMP" space [ "meta" space ]
identifier space timestamp newline ; identifier space timestamp newline ;
identifier = id-chr { id-chr } ; identifier = id-char1 { id-char } ;
id-char1 = ? ASCII letter ? ;
id-char = ? ASCII characters 33..126 except '"#()<>=' ? ; id-char = ? ASCII characters 33..126 except '"#()<>=' ? ;
timestamp = intnum ; timestamp = intnum ;
footer = "/" number newline ; footer = "/" number newline ;