From dac417a38dee2ce5800e8f66406bd08838535dc0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Aug 2020 17:01:59 +0200
Subject: Fix .gitignore after the merge of #12849.

A stray generated file was forgotten.
---
 .gitignore | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 557655317c..92e9fd2105 100644
--- a/.gitignore
+++ b/.gitignore
@@ -154,7 +154,7 @@ plugins/ssr/ssrvernac.ml
 kernel/byterun/coq_instruct.h
 kernel/byterun/coq_jumptbl.h
 kernel/genOpcodeFiles.exe
-kernel/copcodes.ml
+kernel/vmopcodes.ml
 kernel/uint63.ml
 ide/coqide/default.bindings
 ide/coqide/default_bindings_src.exe
-- 
cgit v1.2.3