diff --git a/Maintenance/release_building/public_release_name b/Maintenance/release_building/public_release_name new file mode 100644 index 00000000000..629e657c165 --- /dev/null +++ b/Maintenance/release_building/public_release_name @@ -0,0 +1 @@ +CGAL-5.0