Update URIs following initial push
I changed the name of the repository in gitea so the URIs in the README, dune-project, and partridge.opam files need updating.
This commit is contained in:
@@ -7,11 +7,10 @@ maintainer: ["Matthew Gretton-Dann <matt@gretton-dann.org.uk>"]
|
||||
authors: ["Matthew Gretton-Dann <matt@gretton-dann.org.uk>"]
|
||||
license: "Apache-2.0"
|
||||
tags: ["partridge-problem" "triangular-numbers"]
|
||||
homepage:
|
||||
"https://gitea.gretton-dann.org.uk/mgrettondann/triangle-square-cubes"
|
||||
doc: "https://gitea.gretton-dann.org.uk/mgrettondann/triangle-square-cubes"
|
||||
homepage: "https://gitea.gretton-dann.org.uk/mgrettondann/partridge"
|
||||
doc: "https://gitea.gretton-dann.org.uk/mgrettondann/partridge"
|
||||
bug-reports:
|
||||
"https://gitea.gretton-dann.org.uk/mgrettondann/triangle-square-cubes/issues"
|
||||
"https://gitea.gretton-dann.org.uk/mgrettondann/partridge/issues"
|
||||
depends: [
|
||||
"ocaml" {>= "5.3"}
|
||||
"ocaml-lsp-server" {dev}
|
||||
@@ -37,6 +36,5 @@ build: [
|
||||
"@doc" {with-doc}
|
||||
]
|
||||
]
|
||||
dev-repo:
|
||||
"git+https://gitea.gretton-dann.org.uk/mgrettondann/triangle-square-cubes.git"
|
||||
dev-repo: "git+https://gitea.gretton-dann.org.uk/mgrettondann/partridge.git"
|
||||
x-maintenance-intent: ["(latest)"]
|
||||
|
||||
Reference in New Issue
Block a user