From 59f5e8487e875f111990e61ab2b025f61fbf0d57 Mon Sep 17 00:00:00 2001
From: Arnaud Giersch <arnaud.giersch@iut-bm.univ-fcomte.fr>
Date: Wed, 12 Jun 2013 11:24:37 +0200
Subject: [PATCH] This file doesn't belong to the dist archive.

---
 tools/check_dist_archive.exclude | 1 +
 1 file changed, 1 insertion(+)

diff --git a/tools/check_dist_archive.exclude b/tools/check_dist_archive.exclude
index 61a58e55da..4ded2ab979 100644
--- a/tools/check_dist_archive.exclude
+++ b/tools/check_dist_archive.exclude
@@ -8,6 +8,7 @@
 - Makefile
 - doc/html/.*
 
++ \.cproject
 + \.gitignore
 + README\.(coding|git)
 + mk_win-dist.sh
-- 
2.20.1