Fix makefile.old typo

riscv · Jan 22, 2025 · 0a2678b · 0a2678b
1 parent 80c9e70
commit 0a2678b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Makefile.old b/Makefile.old
@@ -1,4 +1,4 @@
-# WARNING! This Makefile.old is deprecated and has been *mostly* replaced by CMake.
+# WARNING! This Makefile is deprecated and has been *mostly* replaced by CMake.
 # There are some targets related to formal backends (Coq, Hol4, etc.) that have
 # not been fully transitioned, so this is kept for posterity.
 #