mirror of
https://github.com/catchorg/Catch2.git
synced 2025-11-05 06:29:32 +01:00
Rename Catch::Option to Optional
This commit is contained in:
@@ -100,7 +100,7 @@ set(INTERNAL_HEADERS
|
||||
${SOURCES_DIR}/internal/catch_message_info.hpp
|
||||
${SOURCES_DIR}/internal/catch_meta.hpp
|
||||
${SOURCES_DIR}/internal/catch_move_and_forward.hpp
|
||||
${SOURCES_DIR}/internal/catch_option.hpp
|
||||
${SOURCES_DIR}/internal/catch_optional.hpp
|
||||
${SOURCES_DIR}/internal/catch_output_redirect.hpp
|
||||
${SOURCES_DIR}/internal/catch_platform.hpp
|
||||
${SOURCES_DIR}/internal/catch_polyfills.hpp
|
||||
|
||||
Reference in New Issue
Block a user