Remove unneeded header

This commit is contained in:
Juergen Spitzmueller 2020-07-11 16:41:34 +02:00
parent da336cedf3
commit 289cb58f52

View File

@ -11,7 +11,6 @@
*/
#include <config.h>
#include <typeinfo>
#include "InsetBox.h"
#include "InsetCaption.h"