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
History
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
Tip revision: 9f4a2f7
File Mode Size
tests.config -rw-r--r-- 326 bytes

back to top