From dffc9885e54f9c68af23ec79023dfe8516a4cc32 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 16 Sep 2021 14:54:22 +0200
Subject: Add support to clightgen for generating Csyntax AST as .v files

As proposed in #404.

This is presented as a new option `-clight` to the existing `clightgen` tool.

Revise clightgen testing to test the Csyntax output in addition to
the Clight output.
---
 .gitignore | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to '.gitignore')

diff --git a/.gitignore b/.gitignore
index b75ea5e7..99facd7e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -74,7 +74,8 @@
 # MacOS metadata
 .DS_Store
 # Test generated data
-/test/clightgen/*.v
+/test/export/clight/*.v
+/test/export/csyntax/*.v
 # Coq caches
 .lia.cache
 .nia.cache
-- 
cgit