From bfb350e2cd04699893832531f66746d85538896d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 8 Apr 2021 16:14:24 +0200
Subject: Fix a GTK warning in CoqIDE introduced by #14063.

The Variant entry was appearing twice, leading to a duplicate warning.
---
 ide/coqide/coq_commands.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/ide/coqide/coq_commands.ml b/ide/coqide/coq_commands.ml
index 6e02d7fed1..3a080d5f51 100644
--- a/ide/coqide/coq_commands.ml
+++ b/ide/coqide/coq_commands.ml
@@ -93,7 +93,6 @@ let commands = [
    ];
   ["Read Module";
    "Record";
-   "Variant";
    "Remark";
    "Remove LoadPath";
    "Remove Printing Constructor";
-- 
cgit v1.2.3