{"action":"created","issue":{"url":"https://api.github.com/repos/agda/agda/issues/1771","labels_url":"https://api.github.com/repos/agda/agda/issues/1771/labels{/name}","comments_url":"https://api.github.com/repos/agda/agda/issues/1771/comments","events_url":"https://api.github.com/repos/agda/agda/issues/1771/events","html_url":"https://github.com/agda/agda/pull/1771","id":125777936,"number":1771,"title":"added contents of wiki for a variety of stubs","user":{"login":"drull95","id":1316928,"avatar_url":"https://avatars.githubusercontent.com/u/1316928?v=3","gravatar_id":"","url":"https://api.github.com/users/drull95","html_url":"https://github.com/drull95","followers_url":"https://api.github.com/users/drull95/followers","following_url":"https://api.github.com/users/drull95/following{/other_user}","gists_url":"https://api.github.com/users/drull95/gists{/gist_id}","starred_url":"https://api.github.com/users/drull95/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/drull95/subscriptions","organizations_url":"https://api.github.com/users/drull95/orgs","repos_url":"https://api.github.com/users/drull95/repos","events_url":"https://api.github.com/users/drull95/events{/privacy}","received_events_url":"https://api.github.com/users/drull95/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2016-01-09T20:01:29Z","updated_at":"2016-01-21T10:34:14Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/agda/agda/pulls/1771","html_url":"https://github.com/agda/agda/pull/1771","diff_url":"https://github.com/agda/agda/pull/1771.diff","patch_url":"https://github.com/agda/agda/pull/1771.patch"},"body":""},"comment":{"url":"https://api.github.com/repos/agda/agda/issues/comments/173530839","html_url":"https://github.com/agda/agda/pull/1771#issuecomment-173530839","issue_url":"https://api.github.com/repos/agda/agda/issues/1771","id":173530839,"user":{"login":"jespercockx","id":2910371,"avatar_url":"https://avatars.githubusercontent.com/u/2910371?v=3","gravatar_id":"","url":"https://api.github.com/users/jespercockx","html_url":"https://github.com/jespercockx","followers_url":"https://api.github.com/users/jespercockx/followers","following_url":"https://api.github.com/users/jespercockx/following{/other_user}","gists_url":"https://api.github.com/users/jespercockx/gists{/gist_id}","starred_url":"https://api.github.com/users/jespercockx/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jespercockx/subscriptions","organizations_url":"https://api.github.com/users/jespercockx/orgs","repos_url":"https://api.github.com/users/jespercockx/repos","events_url":"https://api.github.com/users/jespercockx/events{/privacy}","received_events_url":"https://api.github.com/users/jespercockx/received_events","type":"User","site_admin":false},"created_at":"2016-01-21T10:34:14Z","updated_at":"2016-01-21T10:34:14Z","body":"So, who decides when this PR can be merged? We shouldn't wait until the merge becomes harder. I can do it if no-one objects."}}