This is an instantiation of an automated benchmark-creating method for Java web applications that mines GitHub.

Settings:
All settings should be configured in Config.java before running anything.
	resultFile		path to the .xml file used as a database. The program creates one if it does not exist
	whitelist		name of the sheet of the resultFile used to store the whitelist
	target			keyword used to mind GitHub. Will also be the name of the sheet in the resultFile where the results are stored
	workspace		path to an empty folder where the post-processing takes place
	sourceDirectory	path to an empty folder where the source code of suitable projects is saved
	binDirectory	path to an empty folder where the executables of suitable projects is saved
	tmpDir			path to an empty folder used to keep temporary information
	gitCredentials	credentials to access the GitHub API with a higher query limit
						for more information: (https://developer.github.com/v3/oauth/)

Functionalities:
	MineGitHub		Should be run first. Creates the .xml database and populates it with repository information: commits, releases, issues, contributors. 
						There is a query limit to the GitHub API so if the functionality times out, wait for an hour and continue.
	MakeCollection	Should always be run after MineGitHub. Reads from the .xml database, and post-processes the repositories. 
						If a repository is suitable, its source is saved in the sourceDirectory. If its executables could be extracted they are saved in the binDirectory
						The .xml database is populated with additional information: build types, library information

