Skip to main content

Browse the archive

Revision 0f7967bd30c718d4290fc4ff7d67c09a4ec3b497 authored by Dzomo the everest Yak on 22 April 2020, 08:20:07 UTC, committed by Dzomo the everest Yak on 22 April 2020, 08:20:07 UTC 
[CI] regenerate hints and dist
1 parent 0bcd4ea
Raw File
.gitattributes 
# Linguist
*.fst linguist-language=FStar
*.fst linguist-documentation=false
*.fsti linguist-language=FStar
*.fsti linguist-documentation=false

# Line endings
Makefile.* eol=lf
Makefile eol=lf
configure eol=lf
.gitignore eol=lf
.ignore eol=lf
*.sh text eol=lf
*.fst eol=lf
*.fsti eol=lf
*.ml* eol=lf
*.hints eol=lf -diff linguist-generated
back to top