From 9b8d01ce7486882bb2fa82b2f328780b9d0ba249 Mon Sep 17 00:00:00 2001
From: Andre Noll <maan@tuebingen.mpg.de>
Date: Sun, 12 Jun 2016 20:38:10 +0200
Subject: [PATCH 1/1] play: Remove unnecessary inclusion of filter.cmdline.h.

This header defines the gengetopt structure of para_filter, which is
not needed for para_play.
---
 play.c | 1 -
 1 file changed, 1 deletion(-)

diff --git a/play.c b/play.c
index e484427c..a7ce563b 100644
--- a/play.c
+++ b/play.c
@@ -13,7 +13,6 @@
 #include "para.h"
 #include "list.h"
 #include "play.cmdline.h"
-#include "filter.cmdline.h"
 #include "error.h"
 #include "ggo.h"
 #include "buffer_tree.h"
-- 
2.39.2