ci: Do not hide ci directory (#6410)

This commit is contained in:
Nikolai Aleksandrovich Pavlov
2017-03-31 15:32:58 +03:00
committed by Justin M. Keyes
parent 77539eef9b
commit a1c928e70c
14 changed files with 12 additions and 12 deletions

View File

@@ -574,7 +574,7 @@ local function gen_itp(it)
if not err then
if allow_failure then
io.stderr:write('Errorred out:\n' .. tostring(emsg) .. '\n')
os.execute([[sh -c "source .ci/common/test.sh ; check_core_dumps --delete \"]] .. Paths.test_luajit_prg .. [[\""]])
os.execute([[sh -c "source ci/common/test.sh ; check_core_dumps --delete \"]] .. Paths.test_luajit_prg .. [[\""]])
else
error(emsg)
end