From d9cc527b3edb3ba39f076ce0b77327a473b89b88 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 8 Oct 2014 18:51:38 -0400 Subject: [PATCH] Remove private header from public driver. --- src/main/main.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/main.cpp b/src/main/main.cpp index e99095855..ca7266b59 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -33,7 +33,6 @@ #include "expr/command.h" #include "util/configuration.h" #include "main/options.h" -#include "theory/uf/options.h" #include "util/output.h" #include "util/result.h" #include "util/statistics.h" -- 2.30.2