Gnome and broken buttons: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Nicolas
imported>Nicolas
m →‎Script: fixed script to consider paths with spaces
Line 27: Line 27:
  export GDK_NATIVE_WINDOWS
  export GDK_NATIVE_WINDOWS
   
   
  SCRIPT_PATH=$(readlink -f $0)
  SCRIPT_PATH=$(readlink -f "$0")
  RODIN_DIR=$(dirname $SCRIPT_PATH)
  RODIN_DIR=$(dirname "$SCRIPT_PATH")
  RODIN_CMD=$RODIN_DIR/rodin
  RODIN_CMD="$RODIN_DIR"/rodin
   
   
  $RODIN_CMD "$@"
  "$RODIN_CMD" "$@"
3. make the file executable:
3. make the file executable:
  chmod +x rodin.sh
  chmod +x rodin.sh

Revision as of 11:02, 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 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" "$@"

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.