From 3a3f11fe1b6c0f059cf2bd0d71aa4deb4a876b26 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 11 Jul 2016 16:49:15 +0200 Subject: ".gitignore" update --- .gitignore | 1 + 1 file changed, 1 insertion(+) (limited to '.gitignore') diff --git a/.gitignore b/.gitignore index 411619080..0d5eee652 100644 --- a/.gitignore +++ b/.gitignore @@ -161,3 +161,4 @@ dev/myinclude /doc/refman/Reference-Manual.optidx /doc/refman/Reference-Manual.optind user-contrib +.*.sw* -- cgit v1.2.3 From ea25e8bcf64caac66bcbd33457ee91d56e80fea3 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 12 Jul 2016 16:32:12 +0200 Subject: .gitignore: no more generated grammar/*.ml files --- .gitignore | 4 ---- 1 file changed, 4 deletions(-) (limited to '.gitignore') diff --git a/.gitignore b/.gitignore index 0d5eee652..8a0c54f8f 100644 --- a/.gitignore +++ b/.gitignore @@ -119,10 +119,6 @@ g_*.ml ide/project_file.ml parsing/compat.ml -grammar/q_util.ml -grammar/tacextend.ml -grammar/vernacextend.ml -grammar/argextend.ml parsing/cLexer.ml ltac/coretactics.ml ltac/extratactics.ml -- cgit v1.2.3