Selecting provers with `Set/Unset Hammer` only works after hammer did run once

[MSoegtropIMC]

I had a minor issue writing test files which check if specific provers are there. This works:

(* This file tests if E-Prover is present *)

From Hammer Require Import Hammer.
Require Import Arith.

(** See https://coqhammer.github.io/#hammer-options *)

(** Specifiy manually which provers/modes to use *)
Set Hammer GSMode 0.

(** Don't run provers in parallel *)
Unset Hammer Parallel.

(** Always run external prover*)
Set Hammer SAutoLimit 0.

(** Prove a lemma using any prover, so that hammer loads and queries provers *)

Lemma lem_1 : le 1 2.
  hammer.
Qed.

(** Use only E-prover *)
Set Hammer Eprover.
Unset Hammer Z3.
Unset Hammer Vampire.
Unset Hammer CVC4.

Lemma lem_2 : forall n : nat, Nat.Odd n \/ Nat.Odd (n + 1).
  Time hammer.
Qed.

but when I remove lem_1, it proves lem_2 with Z3 and not eprover. I guess this is so because the provers are only queried when hammers is used first, which then overwrites the explicit prover selection.

I don't think it is really an issue for anybody, but it would be worthwhile to document it, in case it is hard to fix.