diff options
| author | Théo Zimmermann | 2019-07-20 12:50:17 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-07-20 12:50:17 +0200 |
| commit | cd6fc50854285f02bf151e94bdfb819988531fd2 (patch) | |
| tree | 798fcfd6a0bd529a3d8ae8a25e1c1e62b728be26 /.gitattributes | |
| parent | c80dfb6bd8ff8625ced2cae8b6789707f904a118 (diff) | |
| parent | cf868740c3d18ee9ce9a6b38dd617784625a3cae (diff) | |
Merge PR #9884: doc_grammar, a utility to extract Coq's grammar from .mlg files and insert it into .rst files
Ack-by: Zimmi48
Ack-by: gares
Ack-by: ppedrot
Diffstat (limited to '.gitattributes')
| -rw-r--r-- | .gitattributes | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/.gitattributes b/.gitattributes index 260e3f96b6..415cabba3b 100644 --- a/.gitattributes +++ b/.gitattributes @@ -19,6 +19,7 @@ *.dtd whitespace=blank-at-eol,tab-in-indent dune* whitespace=blank-at-eol,tab-in-indent *.dune whitespace=blank-at-eol,tab-in-indent +*.edit_mlg whitespace=blank-at-eol,tab-in-indent *.el whitespace=blank-at-eol,tab-in-indent *.fake whitespace=blank-at-eol,tab-in-indent *.g whitespace=blank-at-eol,tab-in-indent @@ -36,6 +37,7 @@ dune* whitespace=blank-at-eol,tab-in-indent *.mll whitespace=blank-at-eol,tab-in-indent *.mllib whitespace=blank-at-eol,tab-in-indent *.mlp whitespace=blank-at-eol,tab-in-indent +*.mly whitespace=blank-at-eol,tab-in-indent *.mlpack whitespace=blank-at-eol,tab-in-indent *.nix whitespace=blank-at-eol,tab-in-indent *.nsh whitespace=blank-at-eol,tab-in-indent |