FStarLang/karamel

Review TODO

Closed this issue · 4 comments

I think this is for ancient versions of GCC or maybe in C89 mode where inline is not a keyword. Want me to put a more appropriate comment?

If you are writing a header file to be included in ISO C90 programs, write inline instead of inline. See Alternate Keywords.

(https://gcc.gnu.org/onlinedocs/gcc/Inline.html)

That would be great, thanks! It's more of a note than an actual TODO.

Fixed in 062c33e