Commit b2e92052 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

A fix in the release script.

parent d778d148
......@@ -282,7 +282,7 @@ release:
# Remove files that do not need to (or must not) be distributed.
# Keep because it is used below.
@ git rm \
Makefile dune-workspace.versions \
Makefile \ TODO* \
*.opam coq-menhirlib/descr --quiet
# Hardcode Menhir's version number in the files that need it.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment