Property definitions

github $ PushEvent :: defaultinit
# Triggered when a repository branch is pushed to.
class PushEvent
	super GithubEvent
	serialize

	# SHA of the HEAD commit on the repository.
	var head_commit: Commit is writable

	# Full Git ref that was pushed.
	#
	# Example: “refs/heads/master”
	var ref: String is writable

	# Number of commits in the push.
	var size: nullable Int is writable

	# Array of pushed commits.
	var commits = new Array[Commit] is writable, optional
end
lib/github/events.nit:199,1--217,3