Neels Hofmeyr 18392ee604 jenkins.sh: stay in the jenkins workspace, not in /tmp ... On jenkins, place all logs and manage docker volumes in the workspace instead of a /tmp/* dir. Use $WORKSPACE/logs as docker volume base to begin with, thus there needs to be no copy from /tmp to $WORKSPACE/logs. On non-jenkins runs, place all in a /tmp/* dir still, but also skip copying of the logs: just have a /tmp/logs symlink to the last tmpdir. Change-Id: I8cf6014725ae8ba602be5f3ec31dfb8e49ff993e		2018-05-02 09:36:57 +00:00
..
.release	sysinfo: add missing .release file	2017-08-20 23:41:55 +02:00
Dockerfile	ttcn*test: use log_merge.sh to generate per-testcase merged logs	2018-03-18 13:33:39 +00:00
Makefile	move every 'test network' to its own IP address space	2018-02-06 19:08:45 +01:00
Test.cfg	move every 'test network' to its own IP address space	2018-02-06 19:08:45 +01:00
jenkins.sh	jenkins.sh: stay in the jenkins workspace, not in /tmp	2018-05-02 09:36:57 +00:00