diff options
author | Karl Berry <karl@freefriends.org> | 2018-10-31 20:46:39 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2018-10-31 20:46:39 +0000 |
commit | 4dd72b85bfd4d4b2965492d52e50a45937cc2934 (patch) | |
tree | 6e9a75e1da7a42525039952213f1c82298238db5 /Master/texmf-dist/tex/latex/l3kernel/expl3.lua | |
parent | 804ed7ce7196cf360741cbec749e065de884151d (diff) |
l3 (31oct18)
git-svn-id: svn://tug.org/texlive/trunk@49038 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/tex/latex/l3kernel/expl3.lua')
-rw-r--r-- | Master/texmf-dist/tex/latex/l3kernel/expl3.lua | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/Master/texmf-dist/tex/latex/l3kernel/expl3.lua b/Master/texmf-dist/tex/latex/l3kernel/expl3.lua index 640889bf12a..36b5f631f31 100644 --- a/Master/texmf-dist/tex/latex/l3kernel/expl3.lua +++ b/Master/texmf-dist/tex/latex/l3kernel/expl3.lua @@ -41,7 +41,6 @@ local open = io.open local os_clock = os.clock local os_date = os.date local setcatcode = tex.setcatcode -local str_format = string.format local sprint = tex.sprint local write = tex.write local utf8_char = unicode.utf8.char @@ -61,7 +60,7 @@ local function elapsedtime() if val > 2147483647 then val = 2147483647 end - write(format("%d",val)) + write(format("%d",floor(val))) end l3kernel.elapsedtime = elapsedtime local function resettimer() @@ -110,16 +109,16 @@ local function filemoddate(name) else local hours = floor(off / 60) local mins = abs(off - hours * 60) - timezone = str_format("%+03d", hours) - .. "'" .. str_format("%02d", mins) .. "'" + timezone = format("%+03d", hours) + .. "'" .. format("%02d", mins) .. "'" end write("D:" - .. str_format("%04d", d.year) - .. str_format("%02d", d.month) - .. str_format("%02d", d.day) - .. str_format("%02d", d.hour) - .. str_format("%02d", d.min) - .. str_format("%02d", d.sec) + .. format("%04d", d.year) + .. format("%02d", d.month) + .. format("%02d", d.day) + .. format("%02d", d.hour) + .. format("%02d", d.min) + .. format("%02d", d.sec) .. timezone) end end |