{"action":"opened","issue":{"url":"https://api.github.com/repos/dbuenzli/gg/issues/13","repository_url":"https://api.github.com/repos/dbuenzli/gg","labels_url":"https://api.github.com/repos/dbuenzli/gg/issues/13/labels{/name}","comments_url":"https://api.github.com/repos/dbuenzli/gg/issues/13/comments","events_url":"https://api.github.com/repos/dbuenzli/gg/issues/13/events","html_url":"https://github.com/dbuenzli/gg/issues/13","id":191872156,"number":13,"title":"Box.add_pt","user":{"login":"Chris00","id":1255665,"avatar_url":"https://avatars.githubusercontent.com/u/1255665?v=3","gravatar_id":"","url":"https://api.github.com/users/Chris00","html_url":"https://github.com/Chris00","followers_url":"https://api.github.com/users/Chris00/followers","following_url":"https://api.github.com/users/Chris00/following{/other_user}","gists_url":"https://api.github.com/users/Chris00/gists{/gist_id}","starred_url":"https://api.github.com/users/Chris00/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Chris00/subscriptions","organizations_url":"https://api.github.com/users/Chris00/orgs","repos_url":"https://api.github.com/users/Chris00/repos","events_url":"https://api.github.com/users/Chris00/events{/privacy}","received_events_url":"https://api.github.com/users/Chris00/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2016-11-27T17:04:32Z","updated_at":"2016-11-27T17:04:32Z","closed_at":null,"body":"On thing that would be useful — to me at least — for boxes is to be able to \"add\" a point, i.e., to enlarge a box to make sure it contains an additional point.  Signature  (with maybe a better name):\r\n```ocaml\r\nval add_pt : box -> p -> box\r\n```\r\n(can be implemented for all box types).  Doing it for a collection of points would also be interesting:\r\n```ocaml\r\nval bounding : p list -> box\r\n```"}}
{"actor":{"display_login":"Chris00"}}