From 4e9e4f7177c3c625db3fb3249e31fa81035c2d69 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Tue, 27 Jul 2021 17:12:34 +0200
Subject: [PATCH] Update contributing guidelines wrt flags (#584)

* update guidelines

* oops
---
 CONTRIBUTING.md | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index fafa0c0304..da645bc442 100644
--- 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