|
add_toc_to_github_wiki_page.py
|
improve the script
|
2023-12-21 15:45:39 +01:00 |
|
autotest_cgal_with_ctest
|
fix errors
|
2025-05-26 18:02:24 +02:00 |
|
check_licenses
|
more cleanup
|
2023-11-14 13:41:09 +00:00 |
|
detect_wrong_encoding
|
sed -i -e 's/egrep/grep -E/g'
|
2022-07-01 16:19:36 +02:00 |
|
log.sh
|
fix errors
|
2025-05-26 18:02:24 +02:00 |
|
merge_pr_with_label
|
Improve merge_pr_with_label
|
2021-10-29 17:06:12 +02:00 |
|
tag_pr_per_release.sh
|
fixes post-CGAL-6.0
|
2024-10-01 16:31:06 +02:00 |