Enable the "Edit page on GitHub" buttons

oscar-system · Feb 18, 2024 · 32e993b · 32e993b
1 parent 5d60918
commit 32e993b
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/docs/make_work.jl b/docs/make_work.jl
@@ -166,7 +166,11 @@ function doit(
         end
         src = normpath(root, file)
         dst = normpath(dstbase, relpath(root, srcbase), file)
-        cp(src, dst; force=true)
+        if endswith(file, ".md")
+          symlink(src, dst)
+        else
+          cp(src, dst; force=true)
+        end
         chmod(dst, 0o644)
       end
     end
@@ -198,7 +202,6 @@ function doit(
 
     makedocs(;
       format=Documenter.HTML(;
-        edit_link=nothing, # TODO: make work for imported pages
         prettyurls=!local_build,
         collapselevel=1,
         size_threshold=409600,