--- ray/src/rt/duphead.c	2003/06/05 19:29:34	2.5
+++ ray/src/rt/duphead.c	2003/10/22 02:06:35	2.7
@@ -1,5 +1,5 @@
 #ifndef lint
-static const char	RCSid[] = "$Id: duphead.c,v 2.5 2003/06/05 19:29:34 schorsch Exp $";
+static const char	RCSid[] = "$Id: duphead.c,v 2.7 2003/10/22 02:06:35 greg Exp $";
 #endif
 /*
  * Duplicate header on stdout.
@@ -9,6 +9,7 @@ static const char	RCSid[] = "$Id: duphead.c,v 2.5 2003
 
 #include "copyright.h"
 
+#include  "platform.h"
 #include  "standard.h"
 #include  "paths.h"