Description
A bug happen when selecting a HOST_DIRECTORY different than /codabench. Note that the problem does not occur if the directory on host and inside the container are /codabench.
Let's say we have HOST_DIRECTORY = /home/codabench/ and the desired directory is /codabench/data/temp/. Then makedirs will try to create /home/codabench/data/temp inside the container, which leads to an error.
Fix
A fix was proposed here:
But we should do a proper fix for this bug.
Description
A bug happen when selecting a
HOST_DIRECTORYdifferent than/codabench. Note that the problem does not occur if the directory on host and inside the container are/codabench.Let's say we have
HOST_DIRECTORY = /home/codabench/and the desired directory is/codabench/data/temp/. Thenmakedirswill try to create/home/codabench/data/tempinside the container, which leads to an error.Fix
A fix was proposed here:
But we should do a proper fix for this bug.