diff --git a/Filtered_kernel/dont_submit b/Filtered_kernel/dont_submit
index bbb24e1ee8d..5ab1881467e 100644
--- a/Filtered_kernel/dont_submit
+++ b/Filtered_kernel/dont_submit
@@ -1,2 +1,3 @@
 TODO_static_filters
 Makefile
+Restricted_double.h