Rename dirs

2026-10-19 19:57:05 +02:00
parent 299ee1dfa8
commit 4384d36246
41 changed files with 13 additions and 20 deletions
@@ -0,0 +1,12 @@
+menu "Memory Management options"
+
+config HAVE_MMU
+  bool
+config HAVE_MMU_GENERIC
+  bool
+config HAVE_MMU_SPLIT_ROOT
+  bool
+config HAVE_TLB_SHOOTDOWN_IPI
+  bool
+
+endmenu