Skip to content
Snippets Groups Projects
Commit 38b9f596 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add comment.

parent 9fd57032
No related branches found
No related tags found
1 merge request!419Use `-native-compiler no` to make sure we do not rely on (bugs) in `native_compute`.
Pipeline #74507 passed
......@@ -2,6 +2,7 @@
# `-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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment