# HG changeset patch
# User wenzelm
# Date 940950046 -7200
# Node ID 42836b6c4c737eda90c6c13e05038bd3d4f27e6f
# Parent  80b528790ccc8f76e553b7689f206a7a158366f5
Isabelle %f;

diff -r 80b528790ccc -r 42836b6c4c73 lib/Tools/install
--- a/lib/Tools/install	Tue Oct 26 15:23:25 1999 +0200
+++ b/lib/Tools/install	Tue Oct 26 17:00:46 1999 +0200
@@ -116,7 +116,7 @@
   echo "# KDE Config File" >$KDEAPP || fail "Cannot write file: $KDEAPP"
   echo "[KDE Desktop Entry]" >>$KDEAPP
   echo "Type=Application" >>$KDEAPP
-  echo "Exec=$DISTDIR/bin/Isabelle" >>$KDEAPP
+  echo "Exec=$DISTDIR/bin/Isabelle %f" >>$KDEAPP
   echo "Icon=isabelle.xpm" >>$KDEAPP
   echo "TerminalOptions=" >>$KDEAPP
   echo "Path=" >>$KDEAPP