search

digama0 / mm0

Metamath Zero specification language
Creative Commons Zero v1.0 Universal
306 stars 40 forks source link

Running instrumented `mm0-c` produces different profile file than the one being removed #124

Closed MirceaS closed 1 year ago

MirceaS commented 1 year ago

https://github.com/digama0/mm0/blob/2419f49db68a72d7a8a9fd360dc781d98004ff02/mm0-c/make.sh#L11

Running make.sh on my machine creates the file main.gcda instead of mm0-c-main.gcda and the rm command complains about no file being found to remove. If different architectures produce differently named files, it might be best to replace this command by:

rm -f mm0-c-main.gcda main.gcda