From 1fa37d0a67bb4fd25ebf2e05bbf9d87cd676436f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 2 Oct 2024 20:38:43 +0200
Subject: [PATCH] add comment in _CoqProject

---
 _CoqProject | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/_CoqProject b/_CoqProject
index 40d93206..a47c7168 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -7,7 +7,7 @@
 # Custom flags (to be kept in sync with the dune file at the root of the repo).
 # Fixing this one requires Coq 8.19
 -arg -w -arg -argument-scope-delimiter
-# https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
 -arg -w -arg -notation-incompatible-prefix
 
 stdpp/options.v
-- 
GitLab