Remove comments in docker file

ymherklotz · Jul 12, 2021 · 6edbe20 · 6edbe20
1 parent deb0a4f
commit 6edbe20
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/scripts/docker/Dockerfile b/scripts/docker/Dockerfile
@@ -13,7 +13,7 @@ RUN git clone --recursive https://github.com/ymherklotz/vericert
 
 WORKDIR /vericert
 RUN git checkout -b oopsla21
-#RUN nix-shell --run "make -j7"
-#RUN nix-shell --run "make install"
-#
+RUN nix-shell --run "make -j7"
+RUN nix-shell --run "make install"
+
 RUN echo "export PATH=/vericert/bin:$PATH" >>/root/.bashrc