Skip to content
This repository has been archived by the owner on May 23, 2023. It is now read-only.

rm: cannot remove './nunchaku/tmp*.*': No such file or directory #16

Open
johnyf opened this issue Oct 30, 2017 · 0 comments
Open

rm: cannot remove './nunchaku/tmp*.*': No such file or directory #16

johnyf opened this issue Oct 30, 2017 · 0 comments

Comments

@johnyf
Copy link

johnyf commented Oct 30, 2017

tlapm attempts to remove a non-existent directory related to nunchaku, and prints the output

https://github.com/tlaplus/v2-tlapm/blob/eb830974341821885b1e0c14e81c675543135360/src/tlapm.ml#L154-L157

Although an error is not raised, the output on the command line suggests that there was an error. Printing a message with more information may be helpful to the user.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Development

No branches or pull requests

1 participant