diff options
Diffstat (limited to 'tex/context/base/mkiv/l-os.lua')
-rw-r--r-- | tex/context/base/mkiv/l-os.lua | 21 |
1 files changed, 4 insertions, 17 deletions
diff --git a/tex/context/base/mkiv/l-os.lua b/tex/context/base/mkiv/l-os.lua index cf469f79d..aa04e254d 100644 --- a/tex/context/base/mkiv/l-os.lua +++ b/tex/context/base/mkiv/l-os.lua @@ -227,25 +227,12 @@ local launchers = { } function os.launch(str) - execute(format(launchers[os.name] or launchers.unix,str)) + local command = format(launchers[os.name] or launchers.unix,str) + -- todo: pcall +-- print(command) + execute(command) end -if not os.times then -- ? - -- utime = user time - -- stime = system time - -- cutime = children user time - -- cstime = children system time - function os.times() - return { - utime = os.gettimeofday(), -- user - stime = 0, -- system - cutime = 0, -- children user - cstime = 0, -- children system - } - end -end - - local gettimeofday = os.gettimeofday or os.clock os.gettimeofday = gettimeofday |