From 6b837bc4ca3ed35a5cc8da2d6f2877b6b5967d43 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 5 Oct 2017 10:04:21 +0200 Subject: [PATCH] avoid newline in quoted text --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index a91fb440..9adc844d 100644 --- a/README.md +++ b/README.md @@ -22,8 +22,8 @@ of the dependencies. ## Updating After doing `git pull`, the development may fail to compile because of outdated -dependencies. To fix that, please run `opam update` followed by `make -build-dep`. +dependencies. To fix that, please run `opam update` followed by +`make build-dep`. ## Building Instructions -- GitLab