Skip to content
Snippets Groups Projects
Commit a5701578 authored by Ralf Jung's avatar Ralf Jung
Browse files

revert adding '-native-compiler no' -- it has surprising side-effects for out users

parent 8bf7243a
Branches
Tags
No related merge requests found
Pipeline #75077 canceled
......@@ -2,8 +2,6 @@
# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
-Q stdpp stdpp
-Q stdpp_unstable stdpp.unstable
# Avoid needlessly increasing our trusted code base with native_compute
-arg -native-compiler -arg no
# 'Global Hint Rewrite' not supported before Coq 8.14.
-arg -w -arg -deprecated-hint-rewrite-without-locality
# Fixing this one requires Coq 8.15.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment