clean up documentation directory

Stream: general

[Floris van Doorn]

Question: How do I let my CI cleanup old versions of files generated by doc-gen (specifically the search index).
The reason is that the search carleson#volume_ball_le_of_dist_le leads to https://florisvandoorn.com/carleson/docs/Carleson/HomogeneousType.html#volume_ball_le_of_dist_le
This is a 404 page, but it is the old place where this lemma lives. Now it lives in https://florisvandoorn.com/carleson/docs/Carleson/DoublingMeasure.html#volume_ball_le_of_dist_le

Here is my push CI script. Is fixing this just a matter of deleting docs/docs at the start of the step "Copy documentation to docs/docs"?

[Chris Henson]

Instead of cp I usually use rsync with the --delete flag, which will remove any files that no longer exist.