added push preview in deploydocs

jbcaillau · jbcaillau · commit 45a685faa71c · 2025-07-05T21:19:26.000+02:00
diff --git a/docs/make.jl b/docs/make.jl
@@ -164,4 +164,4 @@ makedocs(;
     plugins=[links],
 )
 
-deploydocs(; repo=repo_url * ".git", devbranch="main")
+deploydocs(; repo = repo_url * ".git", devbranch = "main", push_preview = true)

Original file line number	Diff line number	Diff line change
`@@ -164,4 +164,4 @@ makedocs(;`
`164`	`164`	`plugins=[links],`
`165`	`165`	`)`
`166`	`166`
`167`		`-deploydocs(; repo=repo_url * ".git", devbranch="main")`
	`167`	`+deploydocs(; repo = repo_url * ".git", devbranch = "main", push_preview = true)`