# HG changeset patch
# User wenzelm
# Date 1489931034 -3600
# Node ID cb7cb57c7ce166b8b74cbf39feef1fb7f4645572
# Parent  981df08de0ab03fa7730376c1a91b9d893c402f1
proper primary key;

diff -r 981df08de0ab -r cb7cb57c7ce1 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Mar 19 14:43:17 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Mar 19 14:43:54 2017 +0100
@@ -518,8 +518,9 @@
 
   object Session_Info
   {
+    val session_name = SQL.Column.string("session_name", primary_key = true)
+
     // Build_Log.Session_Info
-    val session_name = SQL.Column.string("session_name")
     val session_timing = SQL.Column.bytes("session_timing")
     val command_timings = SQL.Column.bytes("command_timings")
     val ml_statistics = SQL.Column.bytes("ml_statistics")