Conversation
nojb
left a comment
There was a problem hiding this comment.
LGTM.
Would it be useful if it went into stdune instead?
|
You're right, this bit could actually be moved to stdune. I didn't put it there because the remaining points in #3432 seem a bit specific to dune. Either way works for me! |
|
We could have |
Sounds OK to me, but just in case a second opinion would be nice. |
|
To be fair, putting all temporary files into a single temporary directory seems like a good practice to me. So having a single module that lives in |
|
Yeah makes sense, I'll move it! |
|
Done! |
|
Can I go ahead and merge this despite the CI error? |
|
@NathanReb yeah, this is good to merge. The error is unrelated. |
Signed-off-by: Nathan Rebours <nathan.p.rebours@gmail.com>
This is a first step towards #3432 and is required to move forward with #3392.