X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;ds=sidebyside;f=src%2Fcmdline.c;h=9f1bc9796c639cc80fb97b067648770e9dbe47c8;hb=027eba771a7ef9d25e97f0026d6469ea34c06523;hp=a1a5281c3fb89819f363a99e0273c9a0202232b1;hpb=ff6feef76db1f475195ae50c13afc89ed0a85487;p=pspp

diff --git a/src/cmdline.c b/src/cmdline.c
index a1a5281c3f..9f1bc9796c 100644
--- a/src/cmdline.c
+++ b/src/cmdline.c
@@ -18,6 +18,7 @@
    02111-1307, USA. */
 
 #include <config.h>
+#include "cmdline.h"
 #include <assert.h>
 #include <ctype.h>
 #include <stdio.h>