diff --git a/kernel/register.cc b/kernel/register.cc index 868dbb94..a9e21e6d 100644 --- a/kernel/register.cc +++ b/kernel/register.cc @@ -339,8 +339,11 @@ void Frontend::extra_args(FILE *&f, std::string &filename, std::vector