From 9faad7a44fc6bdc7fcfdbf72f75ec75853bbb611 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lars=20G=C3=B6ttgens?= <lars.goettgens@rwth-aachen.de>
Date: Fri, 16 Feb 2024 19:09:54 +0100
Subject: [PATCH] Enable the "Edit page on GitHub" buttons

---
 docs/make_work.jl | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/docs/make_work.jl b/docs/make_work.jl
index 52a9d6205827..2d11c0048ebf 100644
--- a/docs/make_work.jl
+++ b/docs/make_work.jl
@@ -166,7 +166,7 @@ function doit(
         end
         src = normpath(root, file)
         dst = normpath(dstbase, relpath(root, srcbase), file)
-        cp(src, dst; force=true)
+        symlink(src, dst)
         chmod(dst, 0o644)
       end
     end
@@ -198,7 +198,6 @@ function doit(
 
     makedocs(;
       format=Documenter.HTML(;
-        edit_link=nothing, # TODO: make work for imported pages
         prettyurls=!local_build,
         collapselevel=1,
         size_threshold=409600,