Enable the "Edit page on GitHub" buttons

oscar-system · Feb 16, 2024 · 9faad7a · 9faad7a
1 parent 5d60918
commit 9faad7a
Showing 1 changed file with 1 addition and 2 deletions.
diff --git 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,