Commit 4326f527 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove `-ambiguous-paths` option.

parent 6a295a21
......@@ -8,8 +8,6 @@
-arg -w -arg -convert_concl_no_check
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
# We have ambiguous paths, and live with it.
-arg -w -arg -ambiguous-paths
Markdown is supported
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