Gnome and broken buttons

From Event-B
Revision as of 18:16, 15 January 2010 by imported>Nicolas (New page: A bug in recent versions of Gnome makes buttons not always work within applications, including Eclipse and thus Rodin. This bug is referenced all over the Web in bug reports and forums, fo...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

A bug in recent versions of Gnome makes buttons not always work within applications, including Eclipse and thus Rodin. This bug is referenced all over the Web in bug reports and forums, for instance [[1]].

Workaround

The general workaround (besides waiting for a correction of the bug in GTK), consists in setting a GDK_NATIVE_WINDOWS environment variable to 1 (or true) before starting rodin:

export GDK_NATIVE_WINDOWS=1
/path_to_rodin/rodin

directly in command line.

An alternative is to make it permanent by setting the variable in a configuration file:

  • /etc/profile (requires root privileges)
  • ~/.bashrc if you intend to start rodin always from a terminal

Another way to go is to create a shell script that will initialize the variable and start rodin. Then you will have to use the script instead of the executable.

  • create a file named 'rodin.sh' in the rodin installation directory (in the same directory as the executable)
  • copy/paste the following script:
#!/bin/sh
GDK_NATIVE_WINDOWS=1
export GDK_NATIVE_WINDOWS

SCRIPT_PATH=$(readlink -f $0)
RODIN_DIR=$(dirname $SCRIPT_PATH)
RODIN_CMD=$RODIN_DIR/rodin

$RODIN_CMD "$@"
  • make the file executable:
chmod +x rodin.sh
  • start rodin from the script:
./rodin.sh

You may also make shortcuts point to this script.

A disadvantage of the script is that the variable is unset when the platform restarts, for instance after installing a new feature. Thus, it is recommended to answer NO when the platform offers to restart, then close it and start it again using the script.