Mathieu Arnold 2884d5aa32 Fixup USE_GITHUB usage. ... It already sets DISTNAME to a very nice unique name, do not set it yourself. Sponsored by: Absolight		2016-11-26 10:09:54 +00:00
..
distinfo	Fixup USE_GITHUB usage.	2016-11-26 10:09:54 +00:00
Makefile	Fixup USE_GITHUB usage.	2016-11-26 10:09:54 +00:00
pkg-descr
pkg-plist	lang/polyml: 5.5.2 -> 5.6	2016-04-15 19:58:03 +00:00