Re: history and hotlist not saved; CSS site

On 28/04/17 11:18, Michael Drake wrote:
>
> We could change it not to save the hotlist on exit when
> an external hotlist manager is used, since that would
> be a simple change.

Done.