typo in the documentation of the WARN_ERR flag#104

ybertot wants to merge 1 commit intorocq-community:coq-masterrocq-community/coq-dpdgraph:coq-masterfrom

ybertot:fix-typo-Jun-22ybertot/coq-dpdgraph:fix-typo-Jun-22Copy head branch name to clipboard