Geert-Jan Giezeman 5cd7ceccf1 Replaced w3mir by wget		1999-09-20 08:41:21 +00:00
..
get_cgal_html	Replaced w3mir by wget	1999-09-20 08:41:21 +00:00
send_cgal_mail	…
to_cgal_namespace	…