Commit 4fd6bc8e authored by Christoph Groth's avatar Christoph Groth
Browse files

make extensions page an index page of a subdirectory

This way, the subdirectory can hold individual pages for extensions.
To this end, protect the contents of the extensions directory against
deletion upon deployment.
parent e93076de
Pipeline #16120 passed with stage
in 29 seconds