https://github.com/EasyCrypt/easycrypt
Revision 9f4a2f7c153fe8a1566c8c0ff1bd796083ef587a authored by Pierre-Yves Strub on 03 November 2022, 05:50:59 UTC, committed by Pierre-Yves Strub on 07 November 2022, 20:30:11 UTC
The entry is `file_exclude`. It is a space-separated list of globs. A file is excluded if its basename matches any of the glob. See `fnmatch.fnmatch` of the standard Python libraries to get a description of which glob patterns are supported. Fix #303
1 parent 8d4e67d
Tip revision: 9f4a2f7c153fe8a1566c8c0ff1bd796083ef587a authored by Pierre-Yves Strub on 03 November 2022, 05:50:59 UTC
[ec-runtest]: add the possibility to exclude file based on the name
[ec-runtest]: add the possibility to exclude file based on the name
Tip revision: 9f4a2f7
File | Mode | Size |
---|---|---|
algebra | ||
analysis | ||
core | ||
crypto | ||
datatypes | ||
distributions | ||
encryption | ||
looping | ||
modules | ||
newth | ||
oldlibs | ||
prelude | ||
query_counting | ||
structure | ||
tactics | ||
dune | -rw-r--r-- | 7.3 KB |
Computing file changes ...