From 0d08af47cc0a69331df5e8f2a7dbb40240a2cc6c Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Tue, 8 Dec 2020 12:10:38 +0100 Subject: [PATCH] [headers] remove deleted entry --- headers/header_spec.txt | 1 - 1 file changed, 1 deletion(-) diff --git a/headers/header_spec.txt b/headers/header_spec.txt index d52363f4281..5530a684e62 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -1691,7 +1691,6 @@ src/plugins/wp/doc/coqdoc/typed_generated.tex: .ignore src/plugins/wp/doc/coqdoc/wpcoq.tex: .ignore src/plugins/wp/doc/manual/.gitignore: .ignore src/plugins/wp/doc/manual/Makefile: .ignore -src/plugins/wp/doc/manual/cealistlogo.jpg: .ignore src/plugins/wp/doc/manual/mem.pdf: .ignore src/plugins/wp/doc/manual/size_base.pdf: .ignore src/plugins/wp/doc/manual/size_compl.pdf: .ignore -- GitLab