Fix diff_ci.sh, run CI on folders with Makefile

sosy-lab / sv-benchmarks

Collection of Verification Tasks (MOVED, please follow the link)

https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks

184 stars 169 forks source link

Fix diff_ci.sh, run CI on folders with Makefile #1174

Closed MartinSpiessl closed 4 years ago

MartinSpiessl commented 4 years ago

While the script worked correctly if a folder where things were changed contains NO Makefile, it was broken in cases where it actually contained a Makefile. Then no command was executed for that directory.