summaryrefslogtreecommitdiff
path: root/shell/bin/editor.php
diff options
context:
space:
mode:
authorLuke Shumaker <LukeShu@sbcglobal.net>2011-11-27 11:29:44 -0500
committerLuke Shumaker <LukeShu@sbcglobal.net>2011-11-27 11:29:44 -0500
commitde5cb6329b4e6a4c409d1418f16a3488a53ca953 (patch)
tree3a5af4ef0fd42e4f4904326d2cc94d53582e028e /shell/bin/editor.php
parent76ead734626996f82caddaca57dc2f84243b0947 (diff)
This is what was deployed on the lnns serverHEADmaster
Diffstat (limited to 'shell/bin/editor.php')
-rw-r--r--shell/bin/editor.php50
1 files changed, 25 insertions, 25 deletions
diff --git a/shell/bin/editor.php b/shell/bin/editor.php
index a136cd2..2d5d9c3 100644
--- a/shell/bin/editor.php
+++ b/shell/bin/editor.php
@@ -1,25 +1,25 @@
-<?php
-class p_editor extends prog {
- public static function main($args, $env) {
- if (isset($_POST['stdin'])) {
- if (false) {//if (isset($args[1])) {
- echo $args[0].': saving to `'.$args[1]."'\n";
- file_put_contents($args[1],$_POST['stdin']);
- } else {
- echo $_POST['stdin'];
- }
- } else {
- if (isset($args[1]) && file_exists($args[1])) {
- $text = file_get_contents($args[1]);
- } else {
- $text = '';
- }
- echo '<div class="editor">';
- echo '<input type="hidden" name="stdout_dest" value="'.$_POST['c'].'" />';
- echo '<textarea name="stdin">'.htmlentities($text).'</textarea>'."\n";
- echo '<input type="submit" value="save" />';
- echo '</div>';
- }
- }
-}
-
+<?php
+class p_editor extends prog {
+ public static function main($args, $env) {
+ if (isset($_POST['stdin'])) {
+ if (isset($args[1])) {
+ echo $args[0].': saving to `'.$args[1]."'\n";
+ file_put_contents($args[1],$_POST['stdin']);
+ } else {
+ echo htmlentities($_POST['stdin']);
+ }
+ } else {
+ if (isset($args[1]) && file_exists($args[1])) {
+ $text = file_get_contents($args[1]);
+ } else {
+ $text = '';
+ }
+ echo '<div class="editor">';
+ echo '<input type="hidden" name="stdout_dest" value="'.$_POST['c'].'" />';
+ echo '<textarea name="stdin">'.htmlentities($text).'</textarea>'."\n";
+ echo '<input type="submit" value="save" />';
+ echo '</div>';
+ }
+ }
+}
+