metrics got released, no longer pin-depend

This commit is contained in:
Hannes Mehnert 2020-05-09 22:47:54 +02:00
parent 0920ae142e
commit ab76e1ef89
1 changed files with 3 additions and 8 deletions

View File

@ -29,14 +29,9 @@ depends: [
"duration" "duration"
"decompress" {>= "0.9.0" & < "1.0.0"} "decompress" {>= "0.9.0" & < "1.0.0"}
"checkseum" "checkseum"
"metrics" "metrics" {>= "0.2.0"}
"metrics-lwt" "metrics-lwt" {>= "0.2.0"}
"metrics-influx" "metrics-influx" {>= "0.2.0"}
]
pin-depends: [
["metrics.dev" "git+https://github.com/hannesm/metrics.git#future"]
["metrics-lwt.dev" "git+https://github.com/hannesm/metrics.git#future"]
["metrics-influx.dev" "git+https://github.com/hannesm/metrics.git#future"]
] ]
build: [ build: [
["dune" "subst"] {pinned} ["dune" "subst"] {pinned}