From 4e17878d01010e2537e618d101d1770c12d5fd70 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 1 Nov 2019 10:32:24 -0400 Subject: [PATCH] Stub in a script to return the flags for ghci. --- script/ghci-flags | 2 ++ 1 file changed, 2 insertions(+) create mode 100755 script/ghci-flags diff --git a/script/ghci-flags b/script/ghci-flags new file mode 100755 index 000000000..51a80d953 --- /dev/null +++ b/script/ghci-flags @@ -0,0 +1,2 @@ +#!/bin/bash +# Computes the flags for ghcide to pass to ghci. You probably won’t be running this yourself, but rather ghcide will via configuration in hie.yaml.