From c434c32325059f956794f0899db8b00806bfdb9f Mon Sep 17 00:00:00 2001
From: Dimitri Merejkowsky <d.merej@gmail.com>
Date: Sat, 19 Sep 2020 16:06:51 +0200
Subject: [PATCH] Replace link with contents

I'm pretty sure git won't let me create a pre-push hook this way
---
 pre-push-hook | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)
 mode change 120000 => 100755 pre-push-hook

diff --git a/pre-push-hook b/pre-push-hook
deleted file mode 120000
index ab15986..0000000
--- a/pre-push-hook
+++ /dev/null
@@ -1 +0,0 @@
-.git/hooks/pre-push
\ No newline at end of file
diff --git a/pre-push-hook b/pre-push-hook
new file mode 100755
index 0000000..ac771e1
--- /dev/null
+++ b/pre-push-hook
@@ -0,0 +1,24 @@
+#!/bin/bash
+
+set -e
+
+remote="$1"
+url="$2"
+
+z40=0000000000000000000000000000000000000000
+
+while read local_ref local_sha remote_ref remote_sha
+do
+  if [[ "${local_sha}" = $z40 ]]; then
+    echo "Deleting stuff, nothing to do"
+  else
+    (
+       cd cours
+       poetry run python build.py --clean --werror
+       poetry run python build.py --format pdf
+       poetry run python deploy.py
+    )
+  fi
+done
+
+git lfs pre-push "$@"