diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-02-17 22:41:26 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-02-17 22:41:26 +0100 |
| commit | a91df5fdc60977accd7937eb17b62bd551d3213a (patch) | |
| tree | 982494df3d33609f5eb7c20b41211af1bb89995a /ide/MacOS | |
| parent | 30076f81448721c49b86846de638cbc936c085fb (diff) | |
Remove Whelp commands.
Although these commands were never deprecated, they have been unusable for some
time now, since they send requests to an Italian server which is no longer
alive.
Diffstat (limited to 'ide/MacOS')
| -rw-r--r-- | ide/MacOS/default_accel_map | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map index 6f474eb12..47612cdf7 100644 --- a/ide/MacOS/default_accel_map +++ b/ide/MacOS/default_accel_map @@ -247,7 +247,6 @@ ; (gtk_accel_path "<Actions>/Tactics/Tactic constructor" "") ; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- with" "") ; (gtk_accel_path "<Actions>/Templates/Template Identity Coercion" "") -; (gtk_accel_path "<Actions>/Queries/Whelp Locate" "") (gtk_accel_path "<Actions>/View/Display all low-level contents" "<Shift><Control>l") ; (gtk_accel_path "<Actions>/Tactics/Tactic right" "") ; (gtk_accel_path "<Actions>/Edit/Find Previous" "<Shift>F3") |