Update contributing guidelines wrt flags (#584)

* update guidelines * oops
agda · Jul 27, 2021 · 4e9e4f7 · 4e9e4f7
1 parent d5030a9
commit 4e9e4f7
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -39,9 +39,10 @@ When preparing a PR here are some general guidelines:
 
 - All files should start with
 
-  `{-# OPTIONS --cubical --no-import-sorts --safe #-}`
+  `{-# OPTIONS --safe #-}`
 
-  unless there is a good reason for it not to.
+  unless there is a good reason for it not to. The `--cubical` and
+  `--no-import-sorts` flags are added in the `cubical.agda-lib` file.
 
 - It is much easier for us to review and merge smaller and
   self-contained PRs. If a PR changes a lot of files all over the