comparison vext.sml @ 1718:434be2f0509e output-type-uri

Update vext
author Chris Cannam
date Mon, 26 Jun 2017 11:54:23 +0100
parents e64981b88943
children bf8a5ce8fb62
comparison
equal deleted inserted replaced
1717:1db385567add 1718:434be2f0509e
31 Particular Programs Ltd shall not be used in advertising or 31 Particular Programs Ltd shall not be used in advertising or
32 otherwise to promote the sale, use or other dealings in this 32 otherwise to promote the sale, use or other dealings in this
33 Software without prior written authorization. 33 Software without prior written authorization.
34 *) 34 *)
35 35
36 val vext_version = "0.9.0" 36 val vext_version = "0.9.1"
37 37
38 38
39 datatype vcs = 39 datatype vcs =
40 HG | 40 HG |
41 GIT 41 GIT
1269 String.isPrefix id id_or_tag 1269 String.isPrefix id id_or_tag
1270 then OK true 1270 then OK true
1271 else 1271 else
1272 case git_command_output context libname 1272 case git_command_output context libname
1273 ["rev-list", "-1", id_or_tag] of 1273 ["rev-list", "-1", id_or_tag] of
1274 ERROR e => ERROR e 1274 ERROR e => OK false (* id_or_tag is not an id or tag, but
1275 | OK tid => 1275 that could just mean it hasn't been
1276 OK (tid = id andalso 1276 fetched *)
1277 tid <> id_or_tag) (* else id_or_tag was id not tag *) 1277 | OK tid => OK (tid = id)
1278 1278
1279 fun branch_tip context (libname, branch) = 1279 fun branch_tip context (libname, branch) =
1280 git_command_output context libname 1280 git_command_output context libname
1281 ["rev-list", "-1", 1281 ["rev-list", "-1",
1282 remote_branch_name branch] 1282 remote_branch_name branch]