From 4ee0cedff7726a56ebd53125995a7ae131660b4a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 18 Aug 2020 13:07:54 +0200
Subject: Rename VM-related kernel/cfoo files to kernel/vmfoo

---
 Makefile.build | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index 7806dce79c..4fb4b12be2 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -367,7 +367,7 @@ kernel/byterun/coq_jumptbl.h: kernel/genOpcodeFiles.exe
 	$(SHOW)'WRITE $@'
 	$(HIDE)$< jump > $@
 
-kernel/copcodes.ml: kernel/genOpcodeFiles.exe
+kernel/vmopcodes.ml: kernel/genOpcodeFiles.exe
 	$(SHOW)'WRITE $@'
 	$(HIDE)$< copml > $@
 
-- 
cgit v1.2.3