aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore2
1 files changed, 1 insertions, 1 deletions
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