diff options
| author | Hans Hagen <pragma@wxs.nl> | 2018-03-15 16:04:31 +0100 |
|---|---|---|
| committer | Context Git Mirror Bot <phg42.2a@gmail.com> | 2018-03-15 16:04:31 +0100 |
| commit | a4e07f30e880ab27c2918f81f136e257475b7729 (patch) | |
| tree | 02db002d3001a49777a049f9a98fdc872a5e1ad1 /scripts/context/lua/mtx-plain.lua | |
| parent | cbc37c39432e0ebe38e0922fc6d14c2955ab3ba2 (diff) | |
| download | context-a4e07f30e880ab27c2918f81f136e257475b7729.tar.gz | |
2018-03-15 15:36:00
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(...) |