Skip to content

Commit d74d423

Browse files
tobiasgrosserKha
authored andcommitted
fix: avoid warning by dropping '#pragma once'
Before this change, we would see the warning: "#pragma once in main file"
1 parent 905d320 commit d74d423

File tree

2 files changed

+4
-0
lines changed

2 files changed

+4
-0
lines changed

src/runtime/CMakeLists.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@ if(LLVM)
2424
FILE(READ "${CMAKE_CURRENT_SOURCE_DIR}/../include/lean/lean.h" LEAN_H)
2525
# generate LLVM IR for `static inline` definitions in lean.h for the LLVM backend
2626
string(REPLACE "static inline" "__attribute__((always_inline))" LEAN_H "${LEAN_H}")
27+
# drop '#pragma once' in .c file to avoid warning
28+
string(REPLACE "#pragma once" "" LEAN_H "${LEAN_H}")
2729
file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c" "${LEAN_H}")
2830
message("Generating LLVM bitcode file for Lean runtime at '${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/lean.h.bc'")
2931
add_custom_command(

stage0/src/runtime/CMakeLists.txt

Lines changed: 2 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)