mathieui 9f1e80cd5c Remove force_remote_bookmarks option ... It is 2021, servers ought to not be broken that much.		2021-01-29 11:23:31 +01:00
..
source	Remove force_remote_bookmarks option	2021-01-29 11:23:31 +01:00
stub	doc/stub/potr: remove duplicated declaration	2016-10-21 01:46:26 +02:00
Makefile