From 91198c8e0776e1e204a2b0ad274a7b9282a2080c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20Hakkel?= Date: Mon, 24 Nov 2025 14:17:13 +0100 Subject: [PATCH] Fix deploydocs call in make.jl Generation of documentation was skipped because the optional field `devbranch` was set to "main" instead of "master". Deleting this keyword argument instructs Documenter.jl to figure out the correct branch name automatically. --- docs/make.jl | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/docs/make.jl b/docs/make.jl index f4522f7..c85bdf2 100644 --- a/docs/make.jl +++ b/docs/make.jl @@ -13,7 +13,4 @@ makedocs( ] ) -deploydocs( - repo = "github.com/JuliaFirstOrder/ProximalCore.jl", - devbranch = "main" -) +deploydocs(repo = "github.com/JuliaFirstOrder/ProximalCore.jl")