diff options
| author | Robert Alessi <alessi@robertalessi.net> | 2020-10-07 14:42:17 +0200 |
|---|---|---|
| committer | Robert Alessi <alessi@robertalessi.net> | 2020-10-07 14:42:17 +0200 |
| commit | d672c3818a6b9341e78d6933ade8e1820f46192b (patch) | |
| tree | 04d9c8236c07278c94e9e994040238787b83cf5f | |
| parent | 554560246500a2f7188be20c3be408ff5852ca77 (diff) | |
| download | ekdosis-d672c3818a6b9341e78d6933ade8e1820f46192b.tar.gz | |
bad argument to format in rdgGrp_totei()
| -rw-r--r-- | ekdosis.dtx | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ekdosis.dtx b/ekdosis.dtx index bdc87a5..d08b4a3 100644 --- a/ekdosis.dtx +++ b/ekdosis.dtx | |||
| @@ -8073,7 +8073,7 @@ local function rdgGrp_totei(str) | |||
| 8073 | return rdgGrp_totei(string.format("<%s>%s</%s>", | 8073 | return rdgGrp_totei(string.format("<%s>%s</%s>", |
| 8074 | cmd, arg, cmd)) | 8074 | cmd, arg, cmd)) |
| 8075 | else | 8075 | else |
| 8076 | return rdgGrp_totei(string.format("<%s%s%s%s%s>%s</%s>", | 8076 | return rdgGrp_totei(string.format("<%s%s>%s</%s>", |
| 8077 | cmd, teitype, arg, cmd)) | 8077 | cmd, teitype, arg, cmd)) |
| 8078 | end | 8078 | end |
| 8079 | end) | 8079 | end) |