{"comment":{"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/comments/9684963","html_url":"https://github.com/HOL-Theorem-Prover/HOL/commit/85a05f12bb15f55f4ffb5d40248430c4433d9201#commitcomment-9684963","id":9684963,"user":{"login":"mn200","id":145647,"avatar_url":"https://avatars.githubusercontent.com/u/145647?v=3","gravatar_id":"","url":"https://api.github.com/users/mn200","html_url":"https://github.com/mn200","followers_url":"https://api.github.com/users/mn200/followers","following_url":"https://api.github.com/users/mn200/following{/other_user}","gists_url":"https://api.github.com/users/mn200/gists{/gist_id}","starred_url":"https://api.github.com/users/mn200/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mn200/subscriptions","organizations_url":"https://api.github.com/users/mn200/orgs","repos_url":"https://api.github.com/users/mn200/repos","events_url":"https://api.github.com/users/mn200/events{/privacy}","received_events_url":"https://api.github.com/users/mn200/received_events","type":"User","site_admin":false},"position":null,"line":null,"path":"","commit_id":"85a05f12bb15f55f4ffb5d40248430c4433d9201","created_at":"2015-02-10T22:07:39Z","updated_at":"2015-02-10T22:07:39Z","body":"Urgh.  I didn't realise this was legitimate - that's a new bug in Holmake's behaviour rather than the old one I thought we had been masking in the old system."}}