Marco Ferrari eb688a090c Change directory when checking ignored files (#4933) ... * Change dir when checking ignored files * Set to GITHUB_WORKSPACE		2023-12-06 07:32:46 +00:00
..
functions	Change directory when checking ignored files (#4933)	2023-12-06 07:32:46 +00:00
linter.sh	Don't write colors and logs on disk if not necessary (#4934)	2023-12-05 08:04:13 +00:00