diff options
Diffstat (limited to 'scripts/context/lua/mtx-plain.lua')
| -rw-r--r-- | scripts/context/lua/mtx-plain.lua | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/scripts/context/lua/mtx-plain.lua b/scripts/context/lua/mtx-plain.lua index 347f63f1d..72cc48f92 100644 --- a/scripts/context/lua/mtx-plain.lua +++ b/scripts/context/lua/mtx-plain.lua @@ -49,13 +49,18 @@ scripts = scripts or { } scripts.plain = scripts.plain or { } local passed_options = table.tohash { - "utc" + "utc", + "synctex", } local function execute(...) local command = format(...) report("running command %a\n",command) - return os.execute(command) + statistics.starttiming() + local status = os.execute(command) + statistics.stoptiming() + report("runtime %s seconds",statistics.elapsedtime()) + return status end local function resultof(...) |