chiark / gitweb /
Renamed VECTOR-NULL to NULL-TERMINATED-VECTOR