From 44d1a5a9f71b03d9aceeccd760a63fcdc45f8bad Mon Sep 17 00:00:00 2001 From: hallgren Date: Wed, 12 Oct 2011 17:03:54 +0000 Subject: Improvements of "gf -server" mode and related setup "gf -server" mode now contains everything needed to run the minibar and the grammar editor (including example-based grammar writing). The Setup.hs script installs the required files where gf -server can find them. These files have been moved to a new directory: src/www. The separate server program pgf-http is now obsolete. --- src/runtime/javascript/minibar/feedback.cgi | 44 ----------------------------- 1 file changed, 44 deletions(-) delete mode 100644 src/runtime/javascript/minibar/feedback.cgi (limited to 'src/runtime/javascript/minibar/feedback.cgi') diff --git a/src/runtime/javascript/minibar/feedback.cgi b/src/runtime/javascript/minibar/feedback.cgi deleted file mode 100644 index 0d382f22d..000000000 --- a/src/runtime/javascript/minibar/feedback.cgi +++ /dev/null @@ -1,44 +0,0 @@ -#!/bin/bash - -bin=bin -AUTOHEADER=no -. $bin/cgistart.sh - -save_feedback() { -getquery - -if [ -n "$feedback_path" ] && - echo "t=$(date +%F+%T)&ip=$REMOTE_ADDR&$query&accept_language=$HTTP_ACCEPT_LANGUAGE&user_agent=$(echo -n $HTTP_USER_AGENT | plain2url)" >> "$feedback_path" -then - - pagestart "Thank you!" - echo "Your feedback has been saved." - begin script type="text/javascript" - echo "setTimeout(function(){window.close()},4000);" - end - pageend - -else - - pagestart "Feedback error" - echo "Your feedback could not be saved. Sorry." - p - tag 'input type=button onclick="javascript:history.back()" value="<- Go back"' - pageend - -fi -} - -view_feedback() { - charset="UTF-8" - pagestart "Collected Feedback" - begin pre class=feedbacklist - Reg show reverse drop color_depth,pixel_depth,outer_size,inner_size,available_screen_size from-url <"$PATH_TRANSLATED" | plain2html - end - pageend -} - -case "$PATH_TRANSLATED" in - "") save_feedback ;; - *) view_feedback -esac -- cgit v1.2.3