docker: dump redis on --tmp-dir

[rgaudin]

When using --defrag-redis, we use SAVE to dump redis to filesystem. Currently, redis workdir is hard-coded to /output but it'd be better to use what was passed to --tmp-dir (if passed) as this is an 8GiB file for SO (that we don't delete).

[stale]

This issue has been automatically marked as stale because it has not had recent activity. It will be now be reviewed manually. Thank you for your contributions.

[stale]

This issue has been automatically marked as stale because it has not had recent activity. It will be now be reviewed manually. Thank you for your contributions.