Fix deploydocs call in make.jl (#7)

hakkelt · web-flow · commit f05b087e2f5c · 2025-11-24T16:21:09.000+01:00
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.
diff --git 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")

Original file line number	Diff line number	Diff line change
`@@ -13,7 +13,4 @@ makedocs(`
`13`	`13`	`]`
`14`	`14`	`)`
`15`	`15`
`16`		`-deploydocs(`
`17`		`- repo = "github.com/JuliaFirstOrder/ProximalCore.jl",`
`18`		`- devbranch = "main"`
`19`		`-)`
	`16`	`+deploydocs(repo = "github.com/JuliaFirstOrder/ProximalCore.jl")`