max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/compiler/util): typo at has_inline2_attribute

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-11 14:28:54 -07:00
parent 7461bf9d1d
commit da00dae9df
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/compiler/util.cpp
View file

@ -103,9 +103,9 @@ bool has_inline2_attribute(environment const & env, name const & n) {
if (has_attribute(env, "inline2", n))
return true;
if (is_internal_name(n) && !n.is_atomic()) {
/* Auxiliary declarations such as `f._main` are considered to be marked as `@[inline]`
/* Auxiliary declarations such as `f._main` are considered to be marked as `@[inline2]`
if `f` is marked. */
return has_inline_attribute(env, n.get_prefix());
return has_inline2_attribute(env, n.get_prefix());
}
return false;
}