Ammendment to the last commit: Try to fix documentation on GitHub pages

mirkobunse · mirkobunse · commit 498afe9a66a3 · 2022-12-12T10:36:54.000+01:00
diff --git a/docs/make.jl b/docs/make.jl
@@ -14,4 +14,5 @@ makedocs(;
 
 deploydocs(
     repo = "github.com/mirkobunse/CriticalDifferenceDiagrams.jl.git",
+    devbranch = "main"
 )

Original file line number	Diff line number	Diff line change
`@@ -14,4 +14,5 @@ makedocs(;`
`14`	`14`
`15`	`15`	`deploydocs(`
`16`	`16`	`repo = "github.com/mirkobunse/CriticalDifferenceDiagrams.jl.git",`
	`17`	`+ devbranch = "main"`
`17`	`18`	`)`