fix: avoid warning by dropping '#pragma once' #2007

tobiasgrosser · 2023-01-04T05:37:27Z

Before this change, we would see the warning:

"#pragma once in main file"

Before this change, we would see the warning: "#pragma once in main file"

fix: avoid warning by dropping '#pragma once'

8304433

Before this change, we would see the warning: "#pragma once in main file"

Kha merged commit d74d423 into leanprover:master Jan 4, 2023

tobiasgrosser deleted the remove_pragma_once_warning branch January 4, 2023 08:49

Provide feedback