In commit 892d908 three files were removed. However the deploy system doesn't remove these files from the deployed site so they are still visible. They were no longer visible in the contents but one could arrive there by searching.
This PR manually removes these three files and completes the work of the mentioned commit.
(An alternative would be for the workflow to be updated to deal with deleted files automatically but this wasn't immediately clear to me.)
PatrickMassot
commented
5 months ago
In commit 892d908 three files were removed. However the deploy system doesn't remove these files from the deployed site so they are still visible. They were no longer visible in the contents but one could arrive there by searching.
This PR manually removes these three files and completes the work of the mentioned commit.
(An alternative would be for the workflow to be updated to deal with deleted files automatically but this wasn't immediately clear to me.)