From 2a458c05b491ebb422e48e551b5ed41eb3ef986e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 24 May 2018 03:52:15 +0200 Subject: [misc] Remove leftover files. Dune will complain about these leftovers / dead files in the tree. --- plugins/xml/README | 4 ---- 1 file changed, 4 deletions(-) delete mode 100644 plugins/xml/README (limited to 'plugins') diff --git a/plugins/xml/README b/plugins/xml/README deleted file mode 100644 index 3128189929..0000000000 --- a/plugins/xml/README +++ /dev/null @@ -1,4 +0,0 @@ -The xml export plugin for Coq has been removed from the sources. -A backward compatible plug-in will be provided as a third-party plugin. -For more informations, contact -Claudio Sacerdoti Coen . -- cgit v1.2.3