Take the version number from public_release_name

2019-10-31 18:34:08 +01:00
parent 4f97bd5102
commit 21fedbf0ad
2 changed files with 14 additions and 4 deletions
@@ -154,6 +154,10 @@ foreach(pkg ${files})
    process_package(${pkg})
  endif()
 endforeach()
+if(EXISTS ${GIT_REPO}/Maintenance/release_building/public_release_name)
+  file(COPY "${GIT_REPO}/Maintenance/release_building/public_release_name"
+    DESTINATION "${release_dir}/doc")
+endif()

 #create VERSION
 file(WRITE ${release_dir}/VERSION "${CGAL_VERSION}")