From 09a36ea0b50cb63b2f10e6a4afc882a0e9f0fef3 Mon Sep 17 00:00:00 2001 From: Diederik Dulfer Date: Mon, 14 Jan 2019 19:03:54 +0100 Subject: [PATCH] Add release to github --- .mps/workspace.xml | 22 +++++++++++----------- .travis.yml | 20 +++++++++++++++----- 2 files changed, 26 insertions(+), 16 deletions(-) diff --git a/.mps/workspace.xml b/.mps/workspace.xml index f89ff6f..bb9d79f 100644 --- a/.mps/workspace.xml +++ b/.mps/workspace.xml @@ -1291,22 +1291,24 @@