From 7670ec11be3fd58f83533b6f2418dad82db26f66 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Laurent?= <theo.laurent@inria.fr>
Date: Tue, 2 Jan 2024 16:16:55 +0100
Subject: [PATCH] add comment to DOCKER.md

---
 DOCKER.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/DOCKER.md b/DOCKER.md
index 6c57316..60a5ae8 100644
--- a/DOCKER.md
+++ b/DOCKER.md
@@ -36,3 +36,4 @@ And then to connect (username is 'coq' and password is 'coq' as well):
 ```
 ssh coq@localhost
 ```
+Note you might have to source .profile to get coq in the PATH