From 032999d0b2614091465e6a253a3aed81a5aa9abb Mon Sep 17 00:00:00 2001
From: Antoine Regimbeau <antoine.regimbeau@c-s.fr>
Date: Fri, 26 Apr 2019 17:30:08 +0200
Subject: [PATCH] rename configure option

---
 CI/{configure_option.cmake => configure_options.cmake} | 0
 CI/main_ci.cmake                                       | 2 +-
 2 files changed, 1 insertion(+), 1 deletion(-)
 rename CI/{configure_option.cmake => configure_options.cmake} (100%)

diff --git a/CI/configure_option.cmake b/CI/configure_options.cmake
similarity index 100%
rename from CI/configure_option.cmake
rename to CI/configure_options.cmake
diff --git a/CI/main_ci.cmake b/CI/main_ci.cmake
index eba3829c50..052fae8882 100644
--- a/CI/main_ci.cmake
+++ b/CI/main_ci.cmake
@@ -84,7 +84,7 @@ message(STATUS "CI profile : ${ci_profile}")
 #The following file set the CONFIGURE_OPTIONS variable
 set (ENABLE_DOXYGEN OFF)
 set (CONFIGURE_OPTIONS  "")
-include ( "${CMAKE_CURRENT_LIST_DIR}/configure_option.cmake" )
+include ( "${CMAKE_CURRENT_LIST_DIR}/configure_options.cmake" )
 
 # Sources are already checked out : do nothing for update
 set(CTEST_GIT_UPDATE_CUSTOM echo No update)
-- 
GitLab