Index: kernel/arch/amd64/Makefile.inc
===================================================================
--- kernel/arch/amd64/Makefile.inc	(revision a1b9f63c506357f379bb6f1d9f633d5a740e941c)
+++ 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