From c5dca4b33aff79b7729771555732b4c1387db779 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20P=C3=A4tzel?= <david.paetzel@posteo.de>
Date: Tue, 22 Oct 2019 16:38:01 +0200
Subject: [PATCH] Add ./run script for getting live gnuplot graphs

---
 run | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100755 run

diff --git a/run b/run
new file mode 100755
index 0000000..d6dd919
--- /dev/null
+++ b/run
@@ -0,0 +1,5 @@
+#! /usr/bin/env nix-shell
+#! nix-shell -i fish -p fish feedgnuplot
+
+
+dist-newstyle/build/x86_64-linux/ghc-8.6.5/ga-0.1.0.0/x/ga/build/ga/ga $argv | feedgnuplot --terminal "x11 background '#ffffff'" --domain --stream --lines --xmax 12000 --xmin 0 --xlabel "step" --ylabel "cost" --extracmd "set style line 5 lt rgb 'red' lw 2 pt 6" --style 0 "ls 5"