[m-rev.] diff: remove java library stubs

[Julien Fischer]

Are there any objections to doing the following?

Estimated hours taken: 0.1
Branches: main

Remove the library stub files that we formerly
used for the Java backend.

java/Mmakefile:
	Remove this file.  It's only used to
	build the stub files.

java/library/*.java:
	Delete the Java library stub files.
	We no longer need them now that the real library
	compiles.

Julien.

<I've omitted the diff - it's not very interesting>
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------