Open johnyf opened 7 years ago
tlapm attempts to remove a non-existent directory related to nunchaku, and prints the output
tlapm
nunchaku
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.
tlapmattempts to remove a non-existent directory related tonunchaku, and prints the outputhttps://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.