GitLab

I think it is not needed any more.

* doc/lispref/tindex.pl: Remove file.
* make-dist: No more doc/lispref/tindex.pl.