Stream: Coq devs & plugin devs

Topic: coqdep


view this post on Zulip Jason Gross (May 13 2020 at 19:03):

What's up with

"coqdep" -I . -c "purify_tactic_plugin.mllib" > "purify_tactic_plugin.mllib.d" || ( RV=$?; rm -f "purify_tactic_plugin.mllib.d"; exit $RV )
*** Warning: purify_tactic_plugin.mllib already found in . (discarding ./purify_tactic_plugin.mllib)

?
(in 8.11.1)


Last updated: Oct 16 2021 at 02:03 UTC