diff options
| author | Michael Soegtrop | 2018-12-23 11:39:01 +0100 |
|---|---|---|
| committer | Michael Soegtrop | 2018-12-23 11:39:01 +0100 |
| commit | b878216ca5e85f8164fa098b9dc0e688a212072d (patch) | |
| tree | e0a3f075b94ea7ac1cb6206ea4abbd25892da72d /.gitattributes | |
| parent | 037c9bc18d34de831997278e31511ddcee6a1426 (diff) | |
| parent | 495defa06e59ad64de650e2e0574139d33874730 (diff) | |
Merge PR #9243: Fix line ending issues (azure related)
Diffstat (limited to '.gitattributes')
| -rw-r--r-- | .gitattributes | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/.gitattributes b/.gitattributes index 742ef27f49..47538be4a3 100644 --- a/.gitattributes +++ b/.gitattributes @@ -54,5 +54,5 @@ tools/CoqMakefile.in whitespace=blank-at-eol # CR is desired for these Windows files. *.bat whitespace=cr-at-eol,blank-at-eol,tab-in-indent -* eol=lf -*.bat eol=crlf +# never do endline conversion +* -text |