Fix F12 being turned into F11

The "f11_placeholder" and "f12_placeholder" keys were equals since
31d6a70.

Add an incrementing id into the unused key value to differentiate
placeholder values.
This commit is contained in:
Jules Aguillon 2022-06-24 20:56:04 +02:00
parent ab987c776c
commit d74e8f3b08

View File

@ -231,9 +231,14 @@ final class KeyValue
addKey(name, symbol, KIND_KEYEVENT, code, flags);
}
// Within VALUE_BITS
private static int placeholder_unique_id = 0;
/** Use a unique id as the value because the symbol is shared between every
placeholders (it is the empty string). */
private static void addPlaceholderKey(String name)
{
addKey(name, "", KIND_STRING, 0, 0);
addKey(name, "", KIND_STRING, placeholder_unique_id++, 0);
}
static