search

metamath / metamath-exe

Metamath program - source code for the Metamath executable
GNU General Public License v2.0
75 stars 25 forks source link

Line comments instead of block comments 12 #151

Closed GinoGiotto closed 10 months ago

GinoGiotto commented 1 year ago

Continuation of https://github.com/metamath/metamath-exe/pull/138

This PR covers the mmcmds.c file. Only the header and a few inline comments are left out.

jkingdon commented 1 year ago

At the risk of stating the obvious, // comments came in with C99.

Therefore, the #17 task for "Use // comments instead of /* (or doc-comments where appropriate)" is a special case of "No need to worry about versions of the C language older than C99" from https://github.com/metamath/metamath-exe/blob/master/CONTRIBUTING.md so I don't think there is any need to update CONTRIBUTING or the like as part of this set of changes.

digama0 commented 1 year ago

Well, strictly speaking it's not a special case of the other task which would only support "don't care about /* vs //" rather than "prefer //" which is what this PR series is implementing.

jkingdon commented 1 year ago

Well, strictly speaking it's not a special case of the other task which would only support "don't care about /* vs //" rather than "prefer //" which is what this PR series is implementing.

Strictly speaking, of course that is correct. What the PR series is implementing seems good to me so as far as I can tell we are agreed about what to do.