Index: kernel/arch/amd64/Makefile.inc
===================================================================
--- kernel/arch/amd64/Makefile.inc	(revision fa86fff978f42fa20491d74ff2a6cc904ab53fd0)
+++ kernel/arch/amd64/Makefile.inc	(revision 954c0240b720c64358bccbdcdcb035fdd5a6f347)
@@ -32,4 +32,10 @@
 
 FPU_NO_CFLAGS = -mno-sse -mno-sse2
+
+# TODO: Red Zone is only a problem if we allow interrupts to land on an active
+#       stack. Using separate stack for interrupts and ensuring that we never
+#       enable interrupts on an interrupt stack would allow us to get rid of
+#       the argument.
+
 COMMON_CFLAGS += -mcmodel=$(MEMORY_MODEL) -mno-red-zone -fno-unwind-tables -fno-omit-frame-pointer
 
Index: kernel/arch/arm32/Makefile.inc
===================================================================
--- kernel/arch/arm32/Makefile.inc	(revision fa86fff978f42fa20491d74ff2a6cc904ab53fd0)
+++ kernel/arch/arm32/Makefile.inc	(revision 954c0240b720c64358bccbdcdcb035fdd5a6f347)
@@ -33,5 +33,5 @@
 ATSIGN = %
 
-COMMON_CFLAGS += -fno-omit-frame-pointer -mapcs-frame -march=$(subst _,-,$(PROCESSOR_ARCH)) -mno-unaligned-access -mfpu=vfpv3
+COMMON_CFLAGS += -fno-omit-frame-pointer -mapcs-frame -mcpu=$(subst _,-,$(PROCESSOR)) -mno-unaligned-access -mfpu=vfpv3
 
 ifeq ($(CONFIG_FPU),y)