Parcourir la source

Merge branch 'dev' into 0.1

Leo il y a 10 ans
Parent
commit
3e8bbc0868
8 fichiers modifiés avec 0 ajouts et 12 suppressions
  1. 0 12
      rc_test.json
  2. 0 0
      src/Makefile
  3. 0 0
      src/const.ml
  4. 0 0
      src/exec_cmd.ml
  5. 0 0
      src/file_com.ml
  6. 0 0
      src/oclaunch.ml
  7. 0 0
      src/settings.atd
  8. 0 0
      src/tmp_file.ml

+ 0 - 12
rc_test.json

@@ -1,12 +0,0 @@
-{
-    "progs" : [
-        "task",
-        "echo test",
-        "task +rdv",
-        "vim"
-    ],
-
-    "settings" : [
-        "Todo"
-    ]
-}

Makefile → src/Makefile


const.ml → src/const.ml


exec_cmd.ml → src/exec_cmd.ml


file_com.ml → src/file_com.ml


oclaunch.ml → src/oclaunch.ml


settings.atd → src/settings.atd


tmp_file.ml → src/tmp_file.ml