Difference between revisions of "Gnome and broken buttons"

From Event-B
Jump to navigationJump to search
imported>Nicolas
imported>Nicolas
 
Line 52: Line 52:
  
 
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.
 
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.
 +
 +
Note: the script has been added to official Rodin releases (1.2+) for Linux.

Latest revision as of 13:25, 3 February 2010

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

However, the OS tends to override the value of this variable.

Script

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.

1. create a file named 'rodin.sh' in the rodin installation directory (in the same directory as the executable)

2. copy/paste one of the following scripts (both should work; if one does not, just try the other one) :

#!/bin/sh
GDK_NATIVE_WINDOWS=1
export GDK_NATIVE_WINDOWS

# Compute directory prefix
case "$0" in
	*/*) DIR="`dirname \"$0\"`/" ;;
	*)   DIR=""
esac

"${DIR}rodin" "$@"
#!/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" "$@"

3. make the file executable:

chmod +x rodin.sh

4. 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.

Note: the script has been added to official Rodin releases (1.2+) for Linux.