Difference between pages "Getting Started" and "Gnome and broken buttons"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
m (Fixed double redirect.)
 
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...)
 
Line 1: Line 1:
#REDIRECT [[Developer FAQ]]
+
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 [[https://bugs.eclipse.org/bugs/show_bug.cgi?id=291257|here]].
 +
 
 +
==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.

Revision as of 18:16, 15 January 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

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.