diff --git a/Documentation/html_output_post_processing.py b/Documentation/html_output_post_processing.py index 3e1d3dad87d..22f8e29930e 100755 --- a/Documentation/html_output_post_processing.py +++ b/Documentation/html_output_post_processing.py @@ -219,6 +219,12 @@ removes some unneeded files, and performs minor repair on some glitches.''') for fn in filesjs_files: re_replace_in_file('^.*\[ "Concepts",.*$', '', fn) + dynsections_files=glob.glob('./CGAL.CGAL.*/html/dynsections.js') + for fn in filesjs_files: + re_replace_in_file("'src','ftv2", + "'src','../../CGAL.CGAL/html/ftv2", + fn) + # external is placed by doxygen to mark a class from a tagfile, this # is more confusing then helpful in our case